diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index 544791d60b50f2ccc1be050aa323910955def66c..f82b4ec22a9a6aec054faa65781d2d3505e59942 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -2,34 +2,103 @@
 Field name attributes for builtins (eg: ::) are defined in attributes.ml
 *)
 
-(* Custom pair type *)
-type ('a, 'b) pair =
-| Pair [@f fst, snd] of 'a * 'b
-
+val ( ~+ ) : int -> int
+val ( ~- ) : int -> int
 val ( + ) : int -> int -> int
 val ( - ) : int -> int -> int
 val ( * ) : int -> int -> int
 val ( / ) : int -> int -> int
 
-val ( === ) : 'a -> 'a -> bool
+type fpclass =
+  | FP_normal
+  | FP_subnormal
+  | FP_zero
+  | FP_infinite
+  | FP_nan
+val nan : float
+val infinity : float
+val neg_infinity : float
+val max_float : float
+val ( ~+. ) : float -> float
+val ( ~-. ) : float -> float
+val ( +. ) : float -> float -> float
+val ( -. ) : float -> float -> float
+val ( *. ) : float -> float -> float
+val ( /. ) : float -> float -> float
+val ( ** ) : float -> float -> float
+val abs_float : float -> float
+val mod_float : float -> float -> float
+val atan : float -> float
+val exp : float -> float
+val log : float -> float
+val floor : float -> float
+val min : float -> float -> float
+val max : float -> float -> float
+val classify_float : float -> fpclass
+
+val float_of_int : int -> float
+val float_of_string : string -> float
+val int_of_char : char -> int
+val int_of_float : float -> int
+val string_of_float : float -> string
+val string_of_int : int -> string
+
 val ( < ) : 'a -> 'a -> bool
 val ( > ) : 'a -> 'a -> bool
 val ( <= ) : 'a -> 'a -> bool 
 val ( >= ) : 'a -> 'a -> bool
+val compare : 'a -> 'a -> int
 
 (* Structural equality, need to be careful with implementation *)
 val (=) : 'a -> 'a -> bool
 
+val (^) : string -> string -> string
+
+val ref : 'a -> 'a ref
+val (:=) : 'a ref -> 'a -> unit
+val (!) : 'a ref -> 'a
+
 (* Coq extraction builtins refer directly to Pervasives at times *)
 module Pervasives : sig
   val succ : int -> int
 end
 
+module Int32 : sig
+  val logand : int32 -> int32 -> int32
+  val lognot : int32 -> int32
+  val logor : int32 -> int32 -> int32
+  val logxor : int32 -> int32 -> int32
+  val of_float : float -> int32
+  val shift_left : int32 -> int -> int32
+  val shift_right : int32 -> int -> int32
+  val shift_right_logical : int32 -> int -> int32
+  val to_float : int32 -> float
+end
+
+module Int64 : sig
+  val one : int64
+  val float_of_bits : int64 -> float
+end
+
+(* This may be awkward! *)
+module Lazy : sig
+  type 'a t
+end
+
+module List : sig
+  val map : ('a -> 'b) -> 'a list -> 'b list
+  val rev : 'a list -> 'a list
+end
+
+module String : sig
+  val concat : string -> string list -> string
+  val iter : (char -> unit) -> string -> unit
+  val make : int -> char -> string
+end
+
 (* Coq outputs exceptions in the place of arbitrary *)
 val raise : exn -> 'a
 
-val print : 'a -> unit
-
-val stuck : string -> 'a 
-val to_string : 'a -> string
-val parse : 'a -> 'b
+(* JSRef specific functions *)
+val prerr_string : string -> unit
+val prerr_newline : unit -> unit
diff --git a/generator/tests/jsref/BinInt.ml b/generator/tests/jsref/BinInt.ml
index e7c841e243d912b1eb0d350f957de41e8eab8e71..3fce9d7e6061871febd0932968f37c61aec7c2e7 100644
--- a/generator/tests/jsref/BinInt.ml
+++ b/generator/tests/jsref/BinInt.ml
@@ -3,8 +3,8 @@ open BinPos
 open Bool0
 open Datatypes
 
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
+(*type __ = Obj.t
+let __ = let rec f _ = Obj.repr f in Obj.repr f*)
 
 module Z = 
  struct 
@@ -892,7 +892,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val b2z : bool -> float **)
   
-  let b2z = function
+  let b2z b = match b with
   | true -> 1.
   | false -> 0.
   
diff --git a/generator/tests/jsref/BinNat.ml b/generator/tests/jsref/BinNat.ml
index 596cb84a777b9c30b99642af00314d3b32c065a4..394b02a06c62f3e29aec3b54c4bd1cc2a4d3224c 100644
--- a/generator/tests/jsref/BinNat.ml
+++ b/generator/tests/jsref/BinNat.ml
@@ -3,8 +3,10 @@ open Bool0
 open Datatypes
 open Peano
 
+(*
 type __ = Obj.t
 let __ = let rec f _ = Obj.repr f in Obj.repr f
+*)
 
 module N = 
  struct 
@@ -551,6 +553,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val leb_spec0 : float -> float -> reflect **)
   
+(*
   let leb_spec0 x y =
     iff_reflect (leb x y)
   
@@ -558,6 +561,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   let ltb_spec0 x y =
     iff_reflect (ltb x y)
+*)
   
   module Private_BootStrap = 
    struct 
@@ -619,13 +623,14 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
     mul a (div b (gcd a b))
   
   (** val eqb_spec : float -> float -> reflect **)
-  
+(*
   let eqb_spec x y =
     iff_reflect (eqb x y)
+*)
   
   (** val b2n : bool -> float **)
   
-  let b2n = function
+  let b2n b = match b with
   | true -> 1.
   | false -> 0.
   
@@ -654,6 +659,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
     
    end
   
+(*
   module Private_Dec = 
    struct 
     (** val max_case_strong :
@@ -734,5 +740,6 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   let min_dec =
     Private_Dec.min_dec
+*)
  end
 
diff --git a/generator/tests/jsref/BinPos.ml b/generator/tests/jsref/BinPos.ml
index cba4c2e15193fd268bb373d9eff165b78fe28edf..1a61483f6ec5621c02f96c072dc2dee62b5ee465 100644
--- a/generator/tests/jsref/BinPos.ml
+++ b/generator/tests/jsref/BinPos.ml
@@ -3,8 +3,10 @@ open Bool0
 open Datatypes
 open Peano
 
+(*
 type __ = Obj.t
 let __ = let rec f _ = Obj.repr f in Obj.repr f
+*)
 
 module Pos = 
  struct 
@@ -92,28 +94,28 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val mask_rect : 'a1 -> (float -> 'a1) -> 'a1 -> mask -> 'a1 **)
   
-  let mask_rect f f0 f1 = function
+  let mask_rect f f0 f1 m = match m with
   | IsNul -> f
   | IsPos x -> f0 x
   | IsNeg -> f1
   
   (** val mask_rec : 'a1 -> (float -> 'a1) -> 'a1 -> mask -> 'a1 **)
   
-  let mask_rec f f0 f1 = function
+  let mask_rec f f0 f1 m = match m with
   | IsNul -> f
   | IsPos x -> f0 x
   | IsNeg -> f1
   
   (** val succ_double_mask : mask -> mask **)
   
-  let succ_double_mask = function
+  let succ_double_mask m = match m with
   | IsNul -> IsPos 1.
   | IsPos p -> IsPos ((fun p -> 1. +. (2. *. p)) p)
   | IsNeg -> IsNeg
   
   (** val double_mask : mask -> mask **)
   
-  let double_mask = function
+  let double_mask m = match m with
   | IsNul -> IsNul
   | IsPos p -> IsPos ((fun p -> 2. *. p) p)
   | IsNeg -> IsNeg
@@ -133,7 +135,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val pred_mask : mask -> mask **)
   
-  let pred_mask = function
+  let pred_mask m = match m with
   | IsNul -> IsNeg
   | IsPos q ->
     ((fun f2p1 f2p f1 p ->
@@ -376,8 +378,8 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   (** val sqrtrem_step :
       (float -> float) -> (float -> float) -> (float * mask) -> float * mask **)
   
-  let sqrtrem_step f g = function
-  | (s, y) ->
+  let sqrtrem_step f g p = 
+    let (s, y) = p in
     (match y with
      | IsNul ->
        (((fun p -> 2. *. p) s),
@@ -888,25 +890,21 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
       'a1 -> (float -> coq_PeanoView -> 'a1 -> 'a1) -> float -> coq_PeanoView
       -> 'a1 **)
   
-  let coq_PeanoView_rect f f0 =
-    let rec f1 p = function
+  let rec coq_PeanoView_rect f f0 p p' = match p' with
     | PeanoOne -> f
-    | PeanoSucc (p1, p2) -> f0 p1 p2 (f1 p1 p2)
-    in f1
+    | PeanoSucc (p1, p2) -> f0 p1 p2 (coq_PeanoView_rect f f0 p1 p2)
   
   (** val coq_PeanoView_rec :
       'a1 -> (float -> coq_PeanoView -> 'a1 -> 'a1) -> float -> coq_PeanoView
       -> 'a1 **)
   
-  let coq_PeanoView_rec f f0 =
-    let rec f1 p = function
+  let rec coq_PeanoView_rec f f0 p p' = match p' with
     | PeanoOne -> f
-    | PeanoSucc (p1, p2) -> f0 p1 p2 (f1 p1 p2)
-    in f1
+    | PeanoSucc (p1, p2) -> f0 p1 p2 (coq_PeanoView_rec f f0 p1 p2)
   
   (** val peanoView_xO : float -> coq_PeanoView -> coq_PeanoView **)
   
-  let rec peanoView_xO p = function
+  let rec peanoView_xO p p' = match p' with
   | PeanoOne -> PeanoSucc (1., PeanoOne)
   | PeanoSucc (p0, q0) ->
     PeanoSucc ((succ ((fun p -> 2. *. p) p0)), (PeanoSucc
@@ -914,7 +912,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val peanoView_xI : float -> coq_PeanoView -> coq_PeanoView **)
   
-  let rec peanoView_xI p = function
+  let rec peanoView_xI p p' = match p' with
   | PeanoOne -> PeanoSucc ((succ 1.), (PeanoSucc (1., PeanoOne)))
   | PeanoSucc (p0, q0) ->
     PeanoSucc ((succ ((fun p -> 1. +. (2. *. p)) p0)), (PeanoSucc
@@ -936,27 +934,26 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   (** val coq_PeanoView_iter :
       'a1 -> (float -> 'a1 -> 'a1) -> float -> coq_PeanoView -> 'a1 **)
   
-  let coq_PeanoView_iter a f =
-    let rec iter0 p = function
+  let rec coq_PeanoView_iter a f p p' = match p' with
     | PeanoOne -> a
-    | PeanoSucc (p0, q0) -> f p0 (iter0 p0 q0)
-    in iter0
+    | PeanoSucc (p0, q0) -> f p0 (coq_PeanoView_iter a f p0 q0)
   
   (** val eqb_spec : float -> float -> reflect **)
-  
+(*
   let eqb_spec x y =
     iff_reflect (eqb x y)
+*)
   
   (** val switch_Eq : comparison -> comparison -> comparison **)
   
-  let switch_Eq c = function
+  let switch_Eq c c' = match c' with
   | Eq -> c
   | Lt -> Lt
   | Gt -> Gt
   
   (** val mask2cmp : mask -> comparison **)
   
-  let mask2cmp = function
+  let mask2cmp m = match m with
   | IsNul -> Eq
   | IsPos p0 -> Gt
   | IsNeg -> Lt
@@ -966,6 +963,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
     
    end
   
+(*
   module Private_Dec = 
    struct 
     (** val max_case_strong :
@@ -1046,5 +1044,5 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   let min_dec =
     Private_Dec.min_dec
+*)
  end
-
diff --git a/generator/tests/jsref/BinPosDef.ml b/generator/tests/jsref/BinPosDef.ml
index 130f42a9e1e1eee90d1a6f1ce05a1aafdb244783..1b910c64ad65d3cc30bb50661223cb462843ae2a 100644
--- a/generator/tests/jsref/BinPosDef.ml
+++ b/generator/tests/jsref/BinPosDef.ml
@@ -138,28 +138,28 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val mask_rect : 'a1 -> (float -> 'a1) -> 'a1 -> mask -> 'a1 **)
   
-  let mask_rect f f0 f1 = function
+  let mask_rect f f0 f1 mask = match mask with
   | IsNul -> f
   | IsPos x -> f0 x
   | IsNeg -> f1
   
   (** val mask_rec : 'a1 -> (float -> 'a1) -> 'a1 -> mask -> 'a1 **)
   
-  let mask_rec f f0 f1 = function
+  let mask_rec f f0 f1 mask = match mask with
   | IsNul -> f
   | IsPos x -> f0 x
   | IsNeg -> f1
   
   (** val succ_double_mask : mask -> mask **)
   
-  let succ_double_mask = function
+  let succ_double_mask mask = match mask with
   | IsNul -> IsPos 1.
   | IsPos p -> IsPos ((fun p -> 1. +. (2. *. p)) p)
   | IsNeg -> IsNeg
   
   (** val double_mask : mask -> mask **)
   
-  let double_mask = function
+  let double_mask m = match m with
   | IsNul -> IsNul
   | IsPos p -> IsPos ((fun p -> 2. *. p) p)
   | IsNeg -> IsNeg
@@ -179,7 +179,7 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   (** val pred_mask : mask -> mask **)
   
-  let pred_mask = function
+  let pred_mask m = match m with
   | IsNul -> IsNeg
   | IsPos q ->
     ((fun f2p1 f2p f1 p ->
@@ -477,8 +477,8 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   (** val sqrtrem_step :
       (float -> float) -> (float -> float) -> (float * mask) -> float * mask **)
   
-  let sqrtrem_step f g = function
-  | (s, y) ->
+  let sqrtrem_step f g p =
+  let (s, y) = p in
     (match y with
      | IsNul ->
        (((fun p -> 2. *. p) s),
diff --git a/generator/tests/jsref/Datatypes.ml b/generator/tests/jsref/Datatypes.ml
index 0d18c6b4facd559df13408531d64ec354320e9e9..bcc6b55582e1afad033612792336eb2b6c30076a 100644
--- a/generator/tests/jsref/Datatypes.ml
+++ b/generator/tests/jsref/Datatypes.ml
@@ -4,13 +4,11 @@ let negb b = if b then false else true
 
 (** val fst : ('a1 * 'a2) -> 'a1 **)
 
-let fst p = match p with
-| Pair (x, y) -> x
+let fst p = let (x, y) = p in x
 
 (** val snd : ('a1 * 'a2) -> 'a2 **)
 
-let snd p = match p with
-| Pair (x, y) -> y
+let snd p = let (x, y) = p in y
 
 type comparison =
 | Eq [@f]  (** Auto Generated Attributes **)
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index 411583996992593548d1a686d85543587592fcfb..9baccf42dfdee0900b18248108596aaf51a41c23 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -50,10 +50,10 @@ let ln2 = (log 2.)
 (** val from_string : char list -> number **)
 
 let from_string = (fun s ->
-    try
+    (*try*)
       let s = (String.concat "" (List.map (String.make 1) s)) in
       if s = "" then 0. else float_of_string s
-    with Failure "float_of_string" -> nan)
+    (* FIXME: with Failure "float_of_string" -> nan *) )
    (* Note that we're using `float_of_string' there, which does not have the same
       behavior than JavaScript.  For instance it will read "022" as 22 instead of
       18, which should be the JavaScript result for it. *)
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index 11f0e40ccc04f80c7fad7ca10c662d0932b837e9..61f5a4c25ead09d4b59ad6cb75b9fb17ce3d860d 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -342,8 +342,8 @@ let attributes_accessor_enumerable x = x.attributes_accessor_enumerable
 let attributes_accessor_configurable x = x.attributes_accessor_configurable
 
 type attributes =
-| Coq_attributes_data_ [@f label0] of of attributes_data (** Auto Generated Attributes **)
-| Coq_attributes_accessor_ [@f label0] of of attributes_accessor (** Auto Generated Attributes **)
+| Coq_attributes_data_of [@f label0] of attributes_data (** Auto Generated Attributes **)
+| Coq_attributes_accessor_of [@f label0] of attributes_accessor (** Auto Generated Attributes **)
 
 type descriptor = { descriptor_value : value option;
                     descriptor_writable : bool option;
diff --git a/generator/tests/jsref/LibHeap.ml b/generator/tests/jsref/LibHeap.ml
index 7904a4db1081a3af33c08456bafae95718adf332..e9dcc3a1e05c2efb2b94c28b4bcba640a6d96061 100644
--- a/generator/tests/jsref/LibHeap.ml
+++ b/generator/tests/jsref/LibHeap.ml
@@ -3,8 +3,6 @@ open LibBool
 open LibList
 open LibReflect
 
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
 module type HeapSpec = 
  sig 
   type ('x0, 'x) heap 
@@ -42,8 +40,8 @@ module HeapList =
   
   (** val assoc : 'a1 coq_Comparable -> 'a1 -> ('a1 * 'a2) list -> 'a2 **)
   
-  let rec assoc h1 k = function
-  | [] -> (raise Not_found) __
+  let rec assoc h1 k l = match l with
+  | [] -> raise Not_found
   | p :: l' -> let (x, v) = p in if h1 x k then v else assoc h1 k l'
   
   (** val read : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 **)
@@ -76,7 +74,7 @@ module HeapList =
   (** val mem_assoc :
       'a2 coq_Comparable -> 'a2 -> ('a2 * 'a1) list -> bool **)
   
-  let rec mem_assoc h1 k = function
+  let rec mem_assoc h1 k l = match l with
   | [] -> false
   | p :: l' -> let (x, y) = p in coq_or (h1 x k) (mem_assoc h1 k l')
   
diff --git a/generator/tests/jsref/LibOption.ml b/generator/tests/jsref/LibOption.ml
index 01593ce48c79b384bdee3de2506b77d18ae8f197..a48f5309c2958ea214b06900c111143d1b3bb18e 100644
--- a/generator/tests/jsref/LibOption.ml
+++ b/generator/tests/jsref/LibOption.ml
@@ -22,13 +22,13 @@ let option_comparable h x y =
 
 (** val unsome_default : 'a1 -> 'a1 option -> 'a1 **)
 
-let unsome_default d = function
+let unsome_default d o = match o with
 | Some x -> x
 | None -> d
 
 (** val map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option **)
 
-let map f = function
+let map f o = match o with
 | Some x -> Some (f x)
 | None -> None
 
diff --git a/generator/tests/jsref/LibString.ml b/generator/tests/jsref/LibString.ml
index d5f3b73f9e458396841c7c2749b3b7f671a7bf57..ee203769138cda4372d7b7521972cb76b80395bc 100644
--- a/generator/tests/jsref/LibString.ml
+++ b/generator/tests/jsref/LibString.ml
@@ -3,6 +3,6 @@ open String0
 
 (** val string_comparable : char list coq_Comparable **)
 
-let string_comparable =
-  comparable_of_dec string_dec
+let string_comparable x y =
+  comparable_of_dec string_dec x y
 
diff --git a/generator/tests/jsref/List0.ml b/generator/tests/jsref/List0.ml
index 2dfb950df31a25e17fb6770238b28e699067c0c2..909d21b8614bccbf59828e6e4beb1f29754a8ab3 100644
--- a/generator/tests/jsref/List0.ml
+++ b/generator/tests/jsref/List0.ml
@@ -1,20 +1,18 @@
 (** val hd : 'a1 -> 'a1 list -> 'a1 **)
 
-let hd default = function
+let hd default l = match l with
 | [] -> default
 | x :: l0 -> x
 
 (** val tl : 'a1 list -> 'a1 list **)
 
-let tl = function
+let tl l = match l with
 | [] -> []
 | a :: m -> m
 
 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 
-let map f =
-  let rec map0 = function
+let rec map f l = match l with
   | [] -> []
-  | a :: t -> (f a) :: (map0 t)
-  in map0
+  | a :: t -> (f a) :: (map f t)
 
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index fccb1ccc97bbd43d3fe216c6fa6f339b83d2dbd2..932621cb09bf38953cb152298c45a0dd196f3d90 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -6,7 +6,7 @@ open String0
 
 (** val option_case : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 
-let option_case d f = function
+let option_case d f o = match o with
 | Some x -> f x
 | None -> d
 
@@ -81,7 +81,7 @@ module HeapGen =
   (** val indom_decidable :
       'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> coq_Decidable **)
   
-  let indom_decidable h1 = function
-  | (n, h0) -> Heap.indom_decidable h1 (snd (n, h0))
+  let indom_decidable h1 p =
+    let (n, h0) = p in Heap.indom_decidable h1 (snd (n, h0))
  end