diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index 10a96d264eda974c987aa55f20ea001df890d93f..1d762683d4176cca8b0bf0e76bb35a087e11bdfc 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -10,9 +10,7 @@ open Typedtree
 
 module L = Logged (Token_generator) (struct let size = 256 end)
 
-(**
- * Debug-purpose functions
- *)
+(* TODO: Field annotations for builtin type constructors *)
 
 (**
  * Useful functions (Warning: shadows `show_list' from Mytools)
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index d85d15290349315037afeaba430b43890b47a12e..3b90020cfd556b2ba7c3ad6d39eaeb32e967cb7f 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -4,27 +4,32 @@ type 'a list =
 | :: [@f head, tail] of 'a * 'a list
 *)
 
-val add : 'a -> 'b -> 'c
-val ( + ) : 'a -> 'b -> 'c
-val sub : 'a -> 'a -> 'a
-val ( - ) : 'a -> 'a -> 'a
-val mul : 'a -> 'a -> 'a
-val ( * ) : 'a -> 'a -> 'a
-val div : 'a -> 'a -> 'a
-val ( / ) : 'a -> 'a -> 'a
-                 
-val eq : 'a -> 'a -> bool
+(* Custom pair type *)
+type ('a, 'b) pair =
+| Pair [@f fst, snd] of 'a * 'b
+
+val ( + ) : int -> int -> int
+val ( - ) : int -> int -> int
+val ( * ) : int -> int -> int
+val ( / ) : int -> int -> int
+
 val ( === ) : 'a -> 'a -> bool
-val le : 'a -> 'a -> bool
 val ( < ) : 'a -> 'a -> bool
-val ge : 'a -> 'a -> bool
 val ( > ) : 'a -> 'a -> bool
-
-val leq : 'a -> 'a -> bool
 val ( <= ) : 'a -> 'a -> bool 
-val geq : 'a -> 'a -> bool
 val ( >= ) : 'a -> 'a -> bool
 
+(* Structural equality, need to be careful with implementation *)
+val (=) : 'a -> 'a -> bool
+
+(* Coq extraction builtins refer directly to Pervasives at times *)
+module Pervasives : sig
+  val succ : int -> int
+end
+
+(* Coq outputs exceptions in the place of arbitrary *)
+val raise : exn -> 'a
+
 val print : 'a -> unit
 
 val stuck : string -> 'a 
diff --git a/generator/tests/calc.ml b/generator/tests/calc.ml
index ca9cd11d48866401dd3051e3bb4fa6f81fb94135..5a0daa19b86f93182ad8af6c02b0cda4b9b54fb5 100644
--- a/generator/tests/calc.ml
+++ b/generator/tests/calc.ml
@@ -1,5 +1,3 @@
-open Stack
-
 type expr =
   | Const [@f value] of int
   | Add [@f left, right] of expr * expr
@@ -21,3 +19,7 @@ let rec run expr = match expr with
 and evals sexpr = match sexpr with
   | Emp -> Stack.N
   | Push (v, s) -> Stack.push (run v) (evals s)
+
+let rec mapStack f s = match s with
+  | Stack.N -> Stack.N
+  | Stack.C (x, xs) -> Stack.C (f x, mapStack f xs)
diff --git a/generator/tests/jsref/BinInt.ml b/generator/tests/jsref/BinInt.ml
index 0b89fa5bf655dd6c47aa6ce751c208ff0901f2de..e7c841e243d912b1eb0d350f957de41e8eab8e71 100644
--- a/generator/tests/jsref/BinInt.ml
+++ b/generator/tests/jsref/BinInt.ml
@@ -830,16 +830,6 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
     
    end
   
-  (** val leb_spec0 : float -> float -> reflect **)
-  
-  let leb_spec0 x y =
-    iff_reflect (leb x y)
-  
-  (** val ltb_spec0 : float -> float -> reflect **)
-  
-  let ltb_spec0 x y =
-    iff_reflect (ltb x y)
-  
   module Private_OrderTac = 
    struct 
     module IsTotal = 
@@ -900,11 +890,6 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   let lcm a b =
     abs (mul a (div b (gcd a b)))
   
-  (** val eqb_spec : float -> float -> reflect **)
-  
-  let eqb_spec x y =
-    iff_reflect (eqb x y)
-  
   (** val b2z : bool -> float **)
   
   let b2z = function
@@ -930,91 +915,5 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   
   let ones n =
     pred (shiftl 1. n)
-  
-  module Private_Tac = 
-   struct 
-    
-   end
-  
-  module Private_Dec = 
-   struct 
-    (** val max_case_strong :
-        float -> float -> (float -> float -> __ -> 'a1 -> 'a1) -> (__ -> 'a1)
-        -> (__ -> 'a1) -> 'a1 **)
-    
-    let max_case_strong n m compat hl hr =
-      let c = coq_CompSpec2Type n m (compare n m) in
-      (match c with
-       | CompEqT -> compat m (max n m) __ (hr __)
-       | CompLtT -> compat m (max n m) __ (hr __)
-       | CompGtT -> compat n (max n m) __ (hl __))
-    
-    (** val max_case :
-        float -> float -> (float -> float -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1
-        -> 'a1 **)
-    
-    let max_case n m x x0 x1 =
-      max_case_strong n m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val max_dec : float -> float -> bool **)
-    
-    let max_dec n m =
-      max_case n m (fun x y _ h0 -> if h0 then true else false) true false
-    
-    (** val min_case_strong :
-        float -> float -> (float -> float -> __ -> 'a1 -> 'a1) -> (__ -> 'a1)
-        -> (__ -> 'a1) -> 'a1 **)
-    
-    let min_case_strong n m compat hl hr =
-      let c = coq_CompSpec2Type n m (compare n m) in
-      (match c with
-       | CompEqT -> compat n (min n m) __ (hl __)
-       | CompLtT -> compat n (min n m) __ (hl __)
-       | CompGtT -> compat m (min n m) __ (hr __))
-    
-    (** val min_case :
-        float -> float -> (float -> float -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1
-        -> 'a1 **)
-    
-    let min_case n m x x0 x1 =
-      min_case_strong n m x (fun _ -> x0) (fun _ -> x1)
-    
-    (** val min_dec : float -> float -> bool **)
-    
-    let min_dec n m =
-      min_case n m (fun x y _ h0 -> if h0 then true else false) true false
-   end
-  
-  (** val max_case_strong :
-      float -> float -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let max_case_strong n m x x0 =
-    Private_Dec.max_case_strong n m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val max_case : float -> float -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let max_case n m x x0 =
-    max_case_strong n m (fun _ -> x) (fun _ -> x0)
-  
-  (** val max_dec : float -> float -> bool **)
-  
-  let max_dec =
-    Private_Dec.max_dec
-  
-  (** val min_case_strong :
-      float -> float -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-  
-  let min_case_strong n m x x0 =
-    Private_Dec.min_case_strong n m (fun x1 y _ x2 -> x2) x x0
-  
-  (** val min_case : float -> float -> 'a1 -> 'a1 -> 'a1 **)
-  
-  let min_case n m x x0 =
-    min_case_strong n m (fun _ -> x) (fun _ -> x0)
-  
-  (** val min_dec : float -> float -> bool **)
-  
-  let min_dec =
-    Private_Dec.min_dec
- end
 
+end
diff --git a/generator/tests/jsref/BinPos.ml b/generator/tests/jsref/BinPos.ml
index 1edc64578845e4bbc50260c7e3dce6b4db359dca..cba4c2e15193fd268bb373d9eff165b78fe28edf 100644
--- a/generator/tests/jsref/BinPos.ml
+++ b/generator/tests/jsref/BinPos.ml
@@ -961,16 +961,6 @@ if p <= 1. then f1 () else if mod_float p 2. = 0. then f2p (floor (p /. 2.)) els
   | IsPos p0 -> Gt
   | IsNeg -> Lt
   
-  (** val leb_spec0 : float -> float -> reflect **)
-  
-  let leb_spec0 x y =
-    iff_reflect (leb x y)
-  
-  (** val ltb_spec0 : float -> float -> reflect **)
-  
-  let ltb_spec0 x y =
-    iff_reflect (ltb x y)
-  
   module Private_Tac = 
    struct 
     
diff --git a/generator/tests/jsref/Bool0.ml b/generator/tests/jsref/Bool0.ml
index 22b7a4f050dda1c31eff88bff25cce76fa8b0d82..bc1a977ce6ff8d0fc7f6f09fd12920f0510e681a 100644
--- a/generator/tests/jsref/Bool0.ml
+++ b/generator/tests/jsref/Bool0.ml
@@ -1,16 +1,4 @@
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
 (** val eqb : bool -> bool -> bool **)
 
 let eqb b1 b2 =
   if b1 then if b2 then true else false else if b2 then false else true
-
-type reflect =
-| ReflectT [@f]  (** Auto Generated Attributes **)
-| ReflectF [@f]  (** Auto Generated Attributes **)
-
-(** val iff_reflect : bool -> reflect **)
-
-let iff_reflect b =
-  (if b then (fun _ -> ReflectT) else (fun _ -> ReflectF)) __
-
diff --git a/generator/tests/jsref/Datatypes.ml b/generator/tests/jsref/Datatypes.ml
index 02c38443b480d768f4688e4d9fdc9eb0976c8c40..0d18c6b4facd559df13408531d64ec354320e9e9 100644
--- a/generator/tests/jsref/Datatypes.ml
+++ b/generator/tests/jsref/Datatypes.ml
@@ -1,43 +1,19 @@
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
 (** val negb : bool -> bool **)
 
-let negb = function
-| true -> false
-| false -> true
+let negb b = if b then false else true
 
 (** val fst : ('a1 * 'a2) -> 'a1 **)
 
-let fst = function
-| (x, y) -> x
+let fst p = match p with
+| Pair (x, y) -> x
 
 (** val snd : ('a1 * 'a2) -> 'a2 **)
 
-let snd = function
-| (x, y) -> y
+let snd p = match p with
+| Pair (x, y) -> y
 
 type comparison =
 | Eq [@f]  (** Auto Generated Attributes **)
 | Lt [@f]  (** Auto Generated Attributes **)
 | Gt [@f]  (** Auto Generated Attributes **)
 
-type coq_CompareSpecT =
-| CompEqT [@f]  (** Auto Generated Attributes **)
-| CompLtT [@f]  (** Auto Generated Attributes **)
-| CompGtT [@f]  (** Auto Generated Attributes **)
-
-(** val coq_CompareSpec2Type : comparison -> coq_CompareSpecT **)
-
-let coq_CompareSpec2Type c =
-  (match c with
-   | Eq -> (fun _ -> CompEqT)
-   | Lt -> (fun _ -> CompLtT)
-   | Gt -> (fun _ -> CompGtT)) __
-
-type 'a coq_CompSpecT = coq_CompareSpecT
-
-(** val coq_CompSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 coq_CompSpecT **)
-
-let coq_CompSpec2Type x y c =
-  coq_CompareSpec2Type c
-
diff --git a/generator/tests/jsref/LibBool.ml b/generator/tests/jsref/LibBool.ml
index 10493cd62d0e9b0ed8a13c6681f5011b5cc1bf18..ac7b98837cb493889fbd666e240c6a4333c00bd3 100644
--- a/generator/tests/jsref/LibBool.ml
+++ b/generator/tests/jsref/LibBool.ml
@@ -10,7 +10,5 @@ let coq_or x y =
 
 (** val neg : bool -> bool **)
 
-let neg = function
-| true -> false
-| false -> true
+let neg b = if b then false else true
 
diff --git a/generator/tests/jsref/LibList.ml b/generator/tests/jsref/LibList.ml
index bbfb890e5f42155c1cb4b15a207aed93ffbe8eb5..e34e1e5b0fdf6a586587014b583478a9bc121b84 100644
--- a/generator/tests/jsref/LibList.ml
+++ b/generator/tests/jsref/LibList.ml
@@ -2,88 +2,72 @@ open LibOperation
 open LibReflect
 open Peano
 
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
 (** val list_eq_nil_decidable : 'a1 list -> coq_Decidable **)
 
-let list_eq_nil_decidable = function
+let list_eq_nil_decidable l = match l with
 | [] -> true
 | a :: l0 -> false
 
 (** val fold_right : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
 
-let fold_right f =
-  let rec fold_right0 f0 acc = function
+let rec fold_right f acc l = match l with
   | [] -> acc
-  | x :: l' -> f0 x (fold_right0 f0 acc l')
-  in fold_right0 f
+  | x :: l' -> f x (fold_right f acc l')
 
 (** val fold_left : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
 
-let fold_left f =
-  let rec fold_left0 f0 acc = function
+let rec fold_left f acc l = match l with
   | [] -> acc
-  | x :: l' -> fold_left0 f0 (f0 x acc) l'
-  in fold_left0 f
+  | x :: l' -> fold_left f (f x acc) l'
 
 (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
 
-let map f =
-  let () = () in fold_right (fun x acc -> (f x) :: acc) []
+let map f l =
+  fold_right (fun x acc -> (f x) :: acc) [] l
 
 (** val filter : 'a1 predb -> 'a1 list -> 'a1 list **)
 
-let filter f =
-  let () = () in fold_right (fun x acc -> if f x then x :: acc else acc) []
+let filter f l =
+  fold_right (fun x acc -> if f x then x :: acc else acc) [] l
 
 (** val append : 'a1 list -> 'a1 list -> 'a1 list **)
 
 let append l1 l2 =
-  let () = () in fold_right (fun x acc -> x :: acc) l2 l1
+  fold_right (fun x acc -> x :: acc) l2 l1
 
 (** val concat : 'a1 list list -> 'a1 list **)
 
 let concat l =
-  (let () = () in fold_right append []) l
+  fold_right append [] l
 
 (** val rev : 'a1 list -> 'a1 list **)
 
 let rev l =
-  (let () = () in fold_left (fun x acc -> x :: acc) []) l
+  fold_left (fun x acc -> x :: acc) [] l
 
 (** val length : 'a1 list -> int **)
 
 let length l =
-  (let () = () in fold_right (fun x acc -> plus (Pervasives.succ 0) acc) 0) l
+  fold_right (fun x acc -> plus (Pervasives.succ 0) acc) 0 l
 
 (** val take_drop_last : 'a1 list -> 'a1 list * 'a1 **)
 
-let take_drop_last l =
-  let rec take_drop_last0 = function
-  | [] -> (raise Not_found) __
+let rec take_drop_last l = match l with
+  | [] -> raise Not_found
   | x :: l' ->
     (match l' with
      | [] -> ([], x)
-     | a :: l1 -> let (t, y) = take_drop_last0 l' in ((x :: t), y))
-  in take_drop_last0 l
+     | a :: l1 -> let (t, y) = take_drop_last l' in ((x :: t), y))
 
 (** val nth_def : 'a1 -> int -> 'a1 list -> 'a1 **)
 
-let nth_def d =
-  let rec nth_def0 d0 n = function
-  | [] -> d0
-  | x :: l' ->
-    ((fun fO fS n -> if n=0 then fO () else fS (n-1))
-       (fun _ ->
-       x)
-       (fun n' ->
-       nth_def0 d0 n' l')
-       n)
-  in nth_def0 d
+let rec nth_def d n l = match l with
+  | [] -> d
+  | x :: l' -> if n=0 then x else nth_def d (n-1) l'
 
 (** val mem_decide : 'a1 coq_Comparable -> 'a1 -> 'a1 list -> bool **)
 
-let rec mem_decide h x = function
+let rec mem_decide h x l = match l with
 | [] -> false
 | y :: l' -> if h x y then true else mem_decide h x l'
 
diff --git a/generator/tests/jsref/Peano.ml b/generator/tests/jsref/Peano.ml
index 5f155b5e7e99fafd8e91e1f90746772ee0f79c99..99c30cfb7374b4e394d6f913b80bd269568a2311 100644
--- a/generator/tests/jsref/Peano.ml
+++ b/generator/tests/jsref/Peano.ml
@@ -5,10 +5,5 @@ let rec plus = (+)
 (** val nat_iter : int -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
 
 let rec nat_iter n f x =
-  (fun fO fS n -> if n=0 then fO () else fS (n-1))
-    (fun _ ->
-    x)
-    (fun n' ->
-    f (nat_iter n' f x))
-    n
+  if n=0 then x else f (nat_iter (n-1) f x)
 
diff --git a/generator/tests/jsref/String0.ml b/generator/tests/jsref/String0.ml
index 4b7efded9fea97e87a9413ee61e7e9135bca3864..e802a8f30c82b421aa13425a4f95913f27679d7c 100644
--- a/generator/tests/jsref/String0.ml
+++ b/generator/tests/jsref/String0.ml
@@ -1,18 +1,12 @@
 (** val string_dec : char list -> char list -> bool **)
 
-let string_dec s1 s2 =
-  let rec f = function
-  | [] ->
-    (fun s0 ->
-      match s0 with
-      | [] -> true
-      | a::s3 -> false)
-  | a::s0 ->
-    (fun s3 ->
-      match s3 with
-      | [] -> false
-      | a0::s4 -> if (=) a a0 then if f s0 s4 then true else false else false)
-  in f s1 s2
+let rec string_dec s1 s2 = match s1 with
+  | [] -> (match s2 with
+    | [] -> true
+    | a::s3 -> false)
+  | a::s0 -> (match s2 with
+    | [] -> false
+    | a0::s4 -> if (=) a a0 then string_dec s0 s4 else false)
 
 (** val append : char list -> char list -> char list **)
 
@@ -23,26 +17,19 @@ let rec append s1 s2 =
 
 (** val length : char list -> int **)
 
-let rec length = function
+let rec length l = match l with
 | [] -> 0
 | c::s' -> Pervasives.succ (length s')
 
 (** val substring : int -> int -> char list -> char list **)
 
 let rec substring n m s =
-  (fun fO fS n -> if n=0 then fO () else fS (n-1))
-    (fun _ ->
-    (fun fO fS n -> if n=0 then fO () else fS (n-1))
-      (fun _ ->
-      [])
-      (fun m' ->
-      match s with
+  if n=0 then
+    if m=0 then
+      []
+    else match s with
       | [] -> s
-      | c::s' -> c::(substring 0 m' s'))
-      m)
-    (fun n' ->
-    match s with
+      | c::s' -> c::(substring 0 (m-1) s')
+  else match s with
     | [] -> s
-    | c::s' -> substring n' m s')
-    n
-
+    | c::s' -> substring (n-1) m s'
diff --git a/generator/tests/mylist.ml b/generator/tests/mylist.ml
index 031259b1ed2e27d049312a76316630d6d44c057e..5304e5d2a44fdc4fa5470d3656a0bbefd3216270 100644
--- a/generator/tests/mylist.ml
+++ b/generator/tests/mylist.ml
@@ -1,4 +1,4 @@
-let incr i = add i 1
+let incr i = i + 1
 
 type 'a liste =
   | Nil
@@ -44,8 +44,9 @@ let list0 = Nil
 let list1 = range 0 1 Nil
 let list2 = range 1 5 Nil
 
-let sqr x = mul x x
+let sqr x = x * x
 
+(*
 let print_list l = 
   let rec aux acc l = match l with
     | Nil -> acc
@@ -59,3 +60,4 @@ let f = 1 in
   print (print_list (map (fun x -> x * x) list0));
   print (print_list (map sqr list1));
   print (print_list (map sqr list2));
+  *)