diff --git a/generator/tests/jsref/BinInt.ml b/generator/tests/jsref/BinInt.ml
deleted file mode 100644
index 8aa18110b30ca6bb38f6d11c7711bfc0e17aa225..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/BinInt.ml
+++ /dev/null
@@ -1,924 +0,0 @@
-open BinNat
-open BinPos
-open Bool0
-open Datatypes
-
-(*type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f*)
-
-module Z = 
- struct 
-  type t = float
-  
-      (* HACK *)
-  let is_even p =
-     float_eq (mod_float p 2.) 0.
-
-
-  (** val zero : float **)
-  
-  let zero =
-    0.
-  
-  (** val one : float **)
-  
-  let one =
-    1.
-  
-  (** val two : float **)
-  
-  let two =
-    ((fun p -> 2. *. p) 1.)
-  
-  (** val double : float -> float **)
-  
-  let double x =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p -> ((fun p -> 2. *. p)
-      p))
-      (fun p -> (~-.) ((fun p -> 2. *. p)
-      p))
-      x
-  
-  (** val succ_double : float -> float **)
-  
-  let succ_double x =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      1.)
-      (fun p -> ((fun p -> 1. +. (2. *. p))
-      p))
-      (fun p -> (~-.)
-      (Pos.pred_double p))
-      x
-  
-  (** val pred_double : float -> float **)
-  
-  let pred_double x =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ -> (~-.)
-      1.)
-      (fun p ->
-      (Pos.pred_double p))
-      (fun p -> (~-.) ((fun p -> 1. +. (2. *. p))
-      p))
-      x
-  
-  (** val pos_sub : float -> float -> float **)
-  
-  let rec pos_sub x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        double (pos_sub p q))
-        (fun q ->
-        succ_double (pos_sub p q))
-        (fun _ -> ((fun p -> 2. *. p)
-        p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        pred_double (pos_sub p q))
-        (fun q ->
-        double (pos_sub p q))
-        (fun _ ->
-        (Pos.pred_double p))
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (~-.) ((fun p -> 2. *. p)
-        q))
-        (fun q -> (~-.)
-        (Pos.pred_double q))
-        (fun _ ->
-        0.)
-        y)
-      x
-  
-  (** val add : float -> float -> float **)
-  
-  let add = (+.)
-  
-  (** val opp : float -> float **)
-  
-  let opp = (~-.)
-  
-  (** val succ : float -> float **)
-  
-  let succ = (+.) 1.
-  
-  (** val pred : float -> float **)
-  
-  let pred = (fun x -> x -. 1.)
-  
-  (** val sub : float -> float -> float **)
-  
-  let sub = (-.)
-  
-  (** val mul : float -> float -> float **)
-  
-  let mul = ( *. )
-  
-  (** val pow_pos : float -> float -> float **)
-  
-  let pow_pos z n =
-    Pos.iter n (mul z) 1.
-  
-  (** val pow : float -> float -> float **)
-  
-  let pow x y =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      1.)
-      (fun p ->
-      pow_pos x p)
-      (fun p ->
-      0.)
-      y
-  
-  (** val square : float -> float **)
-  
-  let square x =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      (Pos.square p))
-      (fun p ->
-      (Pos.square p))
-      x
-  
-  (** val compare : float -> float -> comparison **)
-  
-  let compare = fun x y -> if float_eq x y then Eq else if x<y then Lt else Gt
-  
-  (** val sgn : float -> float **)
-  
-  let sgn z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      1.)
-      (fun p -> (~-.)
-      1.)
-      z
-  
-  (** val leb : float -> float -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Eq -> true
-    | Lt -> true
-    | Gt -> false
-  
-  (** val ltb : float -> float -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Eq -> false
-    | Lt -> true
-    | Gt -> false
-  
-  (** val geb : float -> float -> bool **)
-  
-  let geb x y =
-    match compare x y with
-    | Eq -> true
-    | Lt -> false
-    | Gt -> true
-  
-  (** val gtb : float -> float -> bool **)
-  
-  let gtb x y =
-    match compare x y with
-    | Eq -> false
-    | Lt -> false
-    | Gt -> true
-  
-  (** val eqb : float -> float -> bool **)
-  
-  let rec eqb x y =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        true)
-        (fun p ->
-        false)
-        (fun p ->
-        false)
-        y)
-      (fun p ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        false)
-        (fun q ->
-        Pos.eqb p q)
-        (fun p0 ->
-        false)
-        y)
-      (fun p ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        false)
-        (fun p0 ->
-        false)
-        (fun q ->
-        Pos.eqb p q)
-        y)
-      x
-  
-  (** val max : float -> float -> float **)
-  
-  let max = max
-  
-  (** val min : float -> float -> float **)
-  
-  let min = min
-  
-  (** val abs : float -> float **)
-  
-  let abs = abs_float
-  
-  (** val abs_nat : float -> int **)
-  
-  let abs_nat z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0)
-      (fun p ->
-      Pos.to_nat p)
-      (fun p ->
-      Pos.to_nat p)
-      z
-  
-  (** val abs_N : float -> float **)
-  
-  let abs_N z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      p)
-      (fun p ->
-      p)
-      z
-  
-  (** val to_nat : float -> int **)
-  
-  let to_nat z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0)
-      (fun p ->
-      Pos.to_nat p)
-      (fun p ->
-      0)
-      z
-  
-  (** val to_N : float -> float **)
-  
-  let to_N z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      p)
-      (fun p ->
-      0.)
-      z
-  
-  (** val of_nat : int -> float **)
-  
-  let of_nat n =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      0.)
-      (fun n0 ->
-      (Pos.of_succ_nat n0))
-      n
-  
-  (** val of_N : float -> float **)
-  
-  let of_N n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p ->
-      p)
-      n
-  
-  (** val to_pos : float -> float **)
-  
-  let to_pos z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      1.)
-      (fun p ->
-      p)
-      (fun p ->
-      1.)
-      z
-  
-  (** val iter : float -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let iter n f x =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      x)
-      (fun p ->
-      Pos.iter p f x)
-      (fun p ->
-      x)
-      n
-  
-  (** val pos_div_eucl : float -> float -> float * float **)
-  
-  let rec pos_div_eucl a b =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun a' ->
-      let (q, r) = pos_div_eucl a' b in
-      let r' = add (mul ((fun p -> 2. *. p) 1.) r) 1. in
-      if ltb r' b
-      then ((mul ((fun p -> 2. *. p) 1.) q), r')
-      else ((add (mul ((fun p -> 2. *. p) 1.) q) 1.), (sub r' b)))
-      (fun a' ->
-      let (q, r) = pos_div_eucl a' b in
-      let r' = mul ((fun p -> 2. *. p) 1.) r in
-      if ltb r' b
-      then ((mul ((fun p -> 2. *. p) 1.) q), r')
-      else ((add (mul ((fun p -> 2. *. p) 1.) q) 1.), (sub r' b)))
-      (fun _ ->
-      if leb ((fun p -> 2. *. p) 1.) b then (0., 1.) else (1., 0.))
-      a
-  
-  (** val div_eucl : float -> float -> float * float **)
-  
-  let div_eucl a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ -> (0.,
-      0.))
-      (fun a' ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ -> (0.,
-        0.))
-        (fun p ->
-        pos_div_eucl a' b)
-        (fun b' ->
-        let (q, r) = pos_div_eucl a' b' in
-        ((fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-           (fun _ -> ((opp q),
-           0.))
-           (fun p -> ((opp (add q 1.)),
-           (add b r)))
-           (fun p -> ((opp (add q 1.)),
-           (add b r)))
-           r))
-        b)
-      (fun a' ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ -> (0.,
-        0.))
-        (fun p ->
-        let (q, r) = pos_div_eucl a' b in
-        ((fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-           (fun _ -> ((opp q),
-           0.))
-           (fun p0 -> ((opp (add q 1.)),
-           (sub b r)))
-           (fun p0 -> ((opp (add q 1.)),
-           (sub b r)))
-           r))
-        (fun b' ->
-        let (q, r) = pos_div_eucl a' b' in (q, (opp r)))
-        b)
-      a
-  
-  (** val div : float -> float -> float **)
-  
-  let div a b =
-    let (q, x) = div_eucl a b in q
-  
-  (** val modulo : float -> float -> float **)
-  
-  let modulo a b =
-    let (x, r) = div_eucl a b in r
-  
-  (** val quotrem : float -> float -> float * float **)
-  
-  let quotrem a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ -> (0.,
-      0.))
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ -> (0.,
-        a))
-        (fun b0 ->
-        let (q, r) = N.pos_div_eucl a0 b0 in ((of_N q), (of_N r)))
-        (fun b0 ->
-        let (q, r) = N.pos_div_eucl a0 b0 in ((opp (of_N q)), (of_N r)))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ -> (0.,
-        a))
-        (fun b0 ->
-        let (q, r) = N.pos_div_eucl a0 b0 in ((opp (of_N q)), (opp (of_N r))))
-        (fun b0 ->
-        let (q, r) = N.pos_div_eucl a0 b0 in ((of_N q), (opp (of_N r))))
-        b)
-      a
-  
-  (** val quot : float -> float -> float **)
-  
-  let quot a b =
-    fst (quotrem a b)
-  
-  (** val rem : float -> float -> float **)
-  
-  let rem a b =
-    snd (quotrem a b)
-  
-  (** val even : float -> bool **)
-  
-  let even z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      true)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        false)
-        (fun p0 ->
-        true)
-        (fun _ ->
-        false)
-        p)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        false)
-        (fun p0 ->
-        true)
-        (fun _ ->
-        false)
-        p)
-      z
-  
-  (** val odd : float -> bool **)
-  
-  let odd z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      false)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        true)
-        (fun p0 ->
-        false)
-        (fun _ ->
-        true)
-        p)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        true)
-        (fun p0 ->
-        false)
-        (fun _ ->
-        true)
-        p)
-      z
-  
-  (** val div2 : float -> float **)
-  
-  let div2 z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        (Pos.div2 p))
-        (fun p0 ->
-        (Pos.div2 p))
-        (fun _ ->
-        0.)
-        p)
-      (fun p -> (~-.)
-      (Pos.div2_up p))
-      z
-  
-  (** val quot2 : float -> float **)
-  
-  let quot2 z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        (Pos.div2 p))
-        (fun p0 ->
-        (Pos.div2 p))
-        (fun _ ->
-        0.)
-        p)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 -> (~-.)
-        (Pos.div2 p))
-        (fun p0 -> (~-.)
-        (Pos.div2 p))
-        (fun _ ->
-        0.)
-        p)
-      z
-  
-  (** val log2 : float -> float **)
-  
-  let log2 z =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p ->
-        (Pos.size p))
-        (fun p ->
-        (Pos.size p))
-        (fun _ ->
-        0.)
-        p0)
-      (fun p ->
-      0.)
-      z
-  
-  (** val sqrtrem : float -> float * float **)
-  
-  let sqrtrem n =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ -> (0.,
-      0.))
-      (fun p ->
-      let (s, m) = Pos.sqrtrem p in
-      (match m with
-       | Pos.IsNul -> (s, 0.)
-       | Pos.IsPos r -> (s, r)
-       | Pos.IsNeg -> (s, 0.)))
-      (fun p -> (0.,
-      0.))
-      n
-  
-  (** val sqrt : float -> float **)
-  
-  let sqrt n =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun p ->
-      (Pos.sqrt p))
-      (fun p ->
-      0.)
-      n
-  
-  (** val gcd : float -> float -> float **)
-  
-  let gcd a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      abs b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        abs a)
-        (fun b0 ->
-        (Pos.gcd a0 b0))
-        (fun b0 ->
-        (Pos.gcd a0 b0))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        abs a)
-        (fun b0 ->
-        (Pos.gcd a0 b0))
-        (fun b0 ->
-        (Pos.gcd a0 b0))
-        b)
-      a
-  
-  (** val ggcd : float -> float -> float * (float * float) **)
-  
-  let ggcd a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ -> ((abs b), (0.,
-      (sgn b))))
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ -> ((abs a), ((sgn a),
-        0.)))
-        (fun b0 ->
-        let (g, p) = Pos.ggcd a0 b0 in let (aa, bb) = p in (g, (aa, bb)))
-        (fun b0 ->
-        let (g, p) = Pos.ggcd a0 b0 in
-        let (aa, bb) = p in (g, (aa, ((~-.) bb))))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ -> ((abs a), ((sgn a),
-        0.)))
-        (fun b0 ->
-        let (g, p) = Pos.ggcd a0 b0 in
-        let (aa, bb) = p in (g, (((~-.) aa), bb)))
-        (fun b0 ->
-        let (g, p) = Pos.ggcd a0 b0 in
-        let (aa, bb) = p in (g, (((~-.) aa), ((~-.) bb))))
-        b)
-      a
-  
-  (** val testbit : float -> float -> bool **)
-  
-  let testbit a n =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      odd a)
-      (fun p ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        false)
-        (fun a0 ->
-        Pos.testbit a0 p)
-        (fun a0 ->
-        negb (N.testbit (Pos.pred_N a0) p))
-        a)
-      (fun p ->
-      false)
-      n
-  
-  (** val shiftl : float -> float -> float **)
-  
-  let shiftl a n =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      a)
-      (fun p ->
-      Pos.iter p (mul ((fun p -> 2. *. p) 1.)) a)
-      (fun p ->
-      Pos.iter p div2 a)
-      n
-  
-  (** val shiftr : float -> float -> float **)
-  
-  let shiftr a n =
-    shiftl a (opp n)
-  
-  (** val coq_lor : float -> float -> float **)
-  
-  let coq_lor a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        a)
-        (fun b0 ->
-        (Pos.coq_lor a0 b0))
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.ldiff (Pos.pred_N b0) a0)))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        a)
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.ldiff (Pos.pred_N a0) b0)))
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.coq_land (Pos.pred_N a0) (Pos.pred_N b0))))
-        b)
-      a
-  
-  (** val coq_land : float -> float -> float **)
-  
-  let coq_land a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        0.)
-        (fun b0 ->
-        of_N (Pos.coq_land a0 b0))
-        (fun b0 ->
-        of_N (N.ldiff a0 (Pos.pred_N b0)))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        0.)
-        (fun b0 ->
-        of_N (N.ldiff b0 (Pos.pred_N a0)))
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.coq_lor (Pos.pred_N a0) (Pos.pred_N b0))))
-        b)
-      a
-  
-  (** val ldiff : float -> float -> float **)
-  
-  let ldiff a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      0.)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        a)
-        (fun b0 ->
-        of_N (Pos.ldiff a0 b0))
-        (fun b0 ->
-        of_N (N.coq_land a0 (Pos.pred_N b0)))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        a)
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.coq_lor (Pos.pred_N a0) b0)))
-        (fun b0 ->
-        of_N (N.ldiff (Pos.pred_N b0) (Pos.pred_N a0)))
-        b)
-      a
-  
-  (** val coq_lxor : float -> float -> float **)
-  
-  let coq_lxor a b =
-    (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-      (fun _ ->
-      b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        a)
-        (fun b0 ->
-        of_N (Pos.coq_lxor a0 b0))
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.coq_lxor a0 (Pos.pred_N b0))))
-        b)
-      (fun a0 ->
-      (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-        (fun _ ->
-        a)
-        (fun b0 -> (~-.)
-        (N.succ_pos (N.coq_lxor (Pos.pred_N a0) b0)))
-        (fun b0 ->
-        of_N (N.coq_lxor (Pos.pred_N a0) (Pos.pred_N b0)))
-        b)
-      a
-  
-  (** val eq_dec : float -> float -> bool **)
-  
-  let eq_dec x y =
-    ((fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-       (fun _ y0 ->
-       (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-         (fun _ ->
-         true)
-         (fun p ->
-         false)
-         (fun p ->
-         false)
-         y0)
-       (fun x0 y0 ->
-       (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-         (fun _ ->
-         false)
-         (fun p0 ->
-         if Pos.eq_dec x0 p0 then true else false)
-         (fun p0 ->
-         false)
-         y0)
-       (fun x0 y0 ->
-       (fun f0 fp fn z -> if float_eq z 0. then f0 () else if z>0. then fp z else fn (~-. z))
-         (fun _ ->
-         false)
-         (fun p0 ->
-         false)
-         (fun p0 ->
-         if Pos.eq_dec x0 p0 then true else false)
-         y0)
-       x) y
-  
-  module Private_BootStrap = 
-   struct 
-    
-   end
-  
-  module Private_OrderTac = 
-   struct 
-    module IsTotal = 
-     struct 
-      
-     end
-    
-    module Tac = 
-     struct 
-      
-     end
-   end
-  
-  (** val sqrt_up : float -> float **)
-  
-  let sqrt_up a =
-    match compare 0. a with
-    | Eq -> 0.
-    | Lt -> succ (sqrt (pred a))
-    | Gt -> 0.
-  
-  (** val log2_up : float -> float **)
-  
-  let log2_up a =
-    match compare 1. a with
-    | Eq -> 0.
-    | Lt -> succ (log2 (pred a))
-    | Gt -> 0.
-  
-  module Private_NZDiv = 
-   struct 
-    
-   end
-  
-  module Private_Div = 
-   struct 
-    module Quot2Div = 
-     struct 
-      (** val div : float -> float -> float **)
-      
-      let div =
-        quot
-      
-      (** val modulo : float -> float -> float **)
-      
-      let modulo =
-        rem
-     end
-    
-    module NZQuot = 
-     struct 
-      
-     end
-   end
-  
-  (** val lcm : float -> float -> float **)
-  
-  let lcm a b =
-    abs (mul a (div b (gcd a b)))
-  
-  (** val b2z : bool -> float **)
-  
-  let b2z b = match b with
-  | true -> 1.
-  | false -> 0.
-  
-  (** val setbit : float -> float -> float **)
-  
-  let setbit a n =
-    coq_lor a (shiftl 1. n)
-  
-  (** val clearbit : float -> float -> float **)
-  
-  let clearbit a n =
-    ldiff a (shiftl 1. n)
-  
-  (** val lnot : float -> float **)
-  
-  let lnot a =
-    pred (opp a)
-  
-  (** val ones : float -> float **)
-  
-  let ones n =
-    pred (shiftl 1. n)
-
-end
diff --git a/generator/tests/jsref/BinNat.ml b/generator/tests/jsref/BinNat.ml
deleted file mode 100644
index 39688787572012a1ad0b6063548dbd982ff8a007..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/BinNat.ml
+++ /dev/null
@@ -1,749 +0,0 @@
-open BinPos
-open Bool0
-open Datatypes
-open Peano
-
-(*
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-*)
-
-module N = 
- struct 
-  type t = float
-
-    (* HACK *)
-  let is_even p =
-     float_eq (mod_float p 2.) 0.
-
-  (** val zero : float **)
-  
-  let zero =
-    0.
-  
-  (** val one : float **)
-  
-  let one =
-    1.
-  
-  (** val two : float **)
-  
-  let two =
-    ((fun p -> 2. *. p) 1.)
-  
-  (** val succ_double : float -> float **)
-  
-  let succ_double x =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      1.)
-      (fun p -> ((fun p -> 1. +. (2. *. p))
-      p))
-      x
-  
-  (** val double : float -> float **)
-  
-  let double n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p -> ((fun p -> 2. *. p)
-      p))
-      n
-  
-  (** val succ : float -> float **)
-  
-  let succ = (+.) 1.
-  
-  (** val pred : float -> float **)
-  
-  let pred = (fun x -> x -. 1.)
-  
-  (** val succ_pos : float -> float **)
-  
-  let succ_pos n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      1.)
-      (fun p ->
-      Pos.succ p)
-      n
-  
-  (** val add : float -> float -> float **)
-  
-  let add = (+.)
-  
-  (** val sub : float -> float -> float **)
-  
-  let sub = (-.)
-  
-  (** val mul : float -> float -> float **)
-  
-  let mul = ( *. )
-  
-  (** val compare : float -> float -> comparison **)
-  
-  let compare = fun x y -> if float_eq x y then Eq else if x<y then Lt else Gt
-  
-  (** val eqb : float -> float -> bool **)
-  
-  let rec eqb n m =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        true)
-        (fun p ->
-        false)
-        m)
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        false)
-        (fun q ->
-        Pos.eqb p q)
-        m)
-      n
-  
-  (** val leb : float -> float -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Eq -> true
-    | Lt -> true
-    | Gt -> false
-  
-  (** val ltb : float -> float -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Eq -> false
-    | Lt -> true
-    | Gt -> false
-  
-  (** val min : float -> float -> float **)
-  
-  let min = min
-  
-  (** val max : float -> float -> float **)
-  
-  let max = max
-  
-  (** val div2 : float -> float **)
-  
-  let div2 n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p ->
-        p)
-        (fun p ->
-        p)
-        (fun _ ->
-        0.)
-        p0)
-      n
-  
-  (** val even : float -> bool **)
-  
-  let even n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      true)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        false)
-        (fun p0 ->
-        true)
-        (fun _ ->
-        false)
-        p)
-      n
-  
-  (** val odd : float -> bool **)
-  
-  let odd n =
-    negb (even n)
-  
-  (** val pow : float -> float -> float **)
-  
-  let pow n p =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      1.)
-      (fun p0 ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        0.)
-        (fun q ->
-        (Pos.pow q p0))
-        n)
-      p
-  
-  (** val square : float -> float **)
-  
-  let square n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p ->
-      (Pos.square p))
-      n
-  
-  (** val log2 : float -> float **)
-  
-  let log2 n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p ->
-        (Pos.size p))
-        (fun p ->
-        (Pos.size p))
-        (fun _ ->
-        0.)
-        p0)
-      n
-  
-  (** val size : float -> float **)
-  
-  let size n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p ->
-      (Pos.size p))
-      n
-  
-  (** val size_nat : float -> int **)
-  
-  let size_nat n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0)
-      (fun p ->
-      Pos.size_nat p)
-      n
-  
-  (** val pos_div_eucl : float -> float -> float * float **)
-  
-  let rec pos_div_eucl a b =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun a' ->
-      let (q, r) = pos_div_eucl a' b in
-      let r' = succ_double r in
-      if leb b r' then ((succ_double q), (sub r' b)) else ((double q), r'))
-      (fun a' ->
-      let (q, r) = pos_div_eucl a' b in
-      let r' = double r in
-      if leb b r' then ((succ_double q), (sub r' b)) else ((double q), r'))
-      (fun _ ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ -> (0.,
-        1.))
-        (fun p ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p0 -> (0.,
-          1.))
-          (fun p0 -> (0.,
-          1.))
-          (fun _ -> (1.,
-          0.))
-          p)
-        b)
-      a
-  
-  (** val div_eucl : float -> float -> float * float **)
-  
-  let div_eucl a b =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ -> (0.,
-      0.))
-      (fun na ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ -> (0.,
-        a))
-        (fun p ->
-        pos_div_eucl na b)
-        b)
-      a
-  
-  (** val div : float -> float -> float **)
-  
-  let div = (fun x y -> if float_eq x 0. then 0. else floor (x /. y))
-  
-  (** val modulo : float -> float -> float **)
-  
-  let modulo = mod_float
-  
-  (** val gcd : float -> float -> float **)
-  
-  let gcd a b =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      b)
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        a)
-        (fun q ->
-        (Pos.gcd p q))
-        b)
-      a
-  
-  (** val ggcd : float -> float -> float * (float * float) **)
-  
-  let ggcd a b =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ -> (b, (0.,
-      1.)))
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ -> (a, (1.,
-        0.)))
-        (fun q ->
-        let (g, p0) = Pos.ggcd p q in let (aa, bb) = p0 in (g, (aa, bb)))
-        b)
-      a
-  
-  (** val sqrtrem : float -> float * float **)
-  
-  let sqrtrem n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ -> (0.,
-      0.))
-      (fun p ->
-      let (s, m) = Pos.sqrtrem p in
-      (match m with
-       | Pos.IsNul -> (s, 0.)
-       | Pos.IsPos r -> (s, r)
-       | Pos.IsNeg -> (s, 0.)))
-      n
-  
-  (** val sqrt : float -> float **)
-  
-  let sqrt n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p ->
-      (Pos.sqrt p))
-      n
-  
-  (** val coq_lor : float -> float -> float **)
-  
-  let coq_lor n m =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      m)
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        n)
-        (fun q ->
-        (Pos.coq_lor p q))
-        m)
-      n
-  
-  (** val coq_land : float -> float -> float **)
-  
-  let coq_land n m =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        0.)
-        (fun q ->
-        Pos.coq_land p q)
-        m)
-      n
-  
-  (** val ldiff : float -> float -> float **)
-  
-  let rec ldiff n m =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        n)
-        (fun q ->
-        Pos.ldiff p q)
-        m)
-      n
-  
-  (** val coq_lxor : float -> float -> float **)
-  
-  let coq_lxor n m =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      m)
-      (fun p ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        n)
-        (fun q ->
-        Pos.coq_lxor p q)
-        m)
-      n
-  
-  (** val shiftl_nat : float -> int -> float **)
-  
-  let shiftl_nat a n =
-    nat_iter n double a
-  
-  (** val shiftr_nat : float -> int -> float **)
-  
-  let shiftr_nat a n =
-    nat_iter n div2 a
-  
-  (** val shiftl : float -> float -> float **)
-  
-  let shiftl a n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun a0 ->
-      (Pos.shiftl a0 n))
-      a
-  
-  (** val shiftr : float -> float -> float **)
-  
-  let shiftr a n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      a)
-      (fun p ->
-      Pos.iter p div2 a)
-      n
-  
-  (** val testbit_nat : float -> int -> bool **)
-  
-  let testbit_nat a =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ x ->
-      false)
-      (fun p ->
-      Pos.testbit_nat p)
-      a
-  
-  (** val testbit : float -> float -> bool **)
-  
-  let testbit a n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      false)
-      (fun p ->
-      Pos.testbit p n)
-      a
-  
-  (** val to_nat : float -> int **)
-  
-  let to_nat a =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0)
-      (fun p ->
-      Pos.to_nat p)
-      a
-  
-  (** val of_nat : int -> float **)
-  
-  let of_nat n =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      0.)
-      (fun n' ->
-      (Pos.of_succ_nat n'))
-      n
-  
-  (** val iter : float -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let iter n f x =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      x)
-      (fun p ->
-      Pos.iter p f x)
-      n
-  
-  (** val eq_dec : float -> float -> bool **)
-  
-  let eq_dec n m =
-    ((fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-       (fun _ m0 ->
-       (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-         (fun _ ->
-         true)
-         (fun p ->
-         false)
-         m0)
-       (fun x m0 ->
-       (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-         (fun _ ->
-         false)
-         (fun p0 ->
-         if Pos.eq_dec x p0 then true else false)
-         m0)
-       n) m
-  
-  (** val discr : float -> float option **)
-  
-  let discr n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      None)
-      (fun p -> Some
-      p)
-      n
-  
-  (** val binary_rect :
-      'a1 -> (float -> 'a1 -> 'a1) -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let binary_rect f0 f2 fS2 n =
-    let f2' = fun p -> f2 p in
-    let fS2' = fun p -> fS2 p in
-    ((fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-       (fun _ ->
-       f0)
-       (fun p ->
-       let rec f p0 =
-         (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-           (fun p1 ->
-           fS2' p1 (f p1))
-           (fun p1 ->
-           f2' p1 (f p1))
-           (fun _ ->
-           fS2 0. f0)
-           p0
-       in f p)
-       n)
-  
-  (** val binary_rec :
-      'a1 -> (float -> 'a1 -> 'a1) -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let binary_rec =
-    binary_rect
-  
-  (** val peano_rect : 'a1 -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let peano_rect f0 f n =
-    let f' = fun p -> f p in
-    ((fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-       (fun _ ->
-       f0)
-       (fun p ->
-       Pos.peano_rect (f 0. f0) f' p)
-       n)
-  
-  (** val peano_rec : 'a1 -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let peano_rec =
-    peano_rect
-  
-  (** 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_BootStrap = 
-   struct 
-    
-   end
-  
-  (** val recursion : 'a1 -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let recursion x =
-    peano_rect x
-  
-  module Private_OrderTac = 
-   struct 
-    module IsTotal = 
-     struct 
-      
-     end
-    
-    module Tac = 
-     struct 
-      
-     end
-   end
-  
-  module Private_NZPow = 
-   struct 
-    
-   end
-  
-  module Private_NZSqrt = 
-   struct 
-    
-   end
-  
-  (** val sqrt_up : float -> float **)
-  
-  let sqrt_up a =
-    match compare 0. a with
-    | Eq -> 0.
-    | Lt -> succ (sqrt (pred a))
-    | Gt -> 0.
-  
-  (** val log2_up : float -> float **)
-  
-  let log2_up a =
-    match compare 1. a with
-    | Eq -> 0.
-    | Lt -> succ (log2 (pred a))
-    | Gt -> 0.
-  
-  module Private_NZDiv = 
-   struct 
-    
-   end
-  
-  (** val lcm : float -> float -> float **)
-  
-  let lcm a b =
-    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 b = match b with
-  | true -> 1.
-  | false -> 0.
-  
-  (** val setbit : float -> float -> float **)
-  
-  let setbit a n =
-    coq_lor a (shiftl 1. n)
-  
-  (** val clearbit : float -> float -> float **)
-  
-  let clearbit a n =
-    ldiff a (shiftl 1. n)
-  
-  (** val ones : float -> float **)
-  
-  let ones n =
-    pred (shiftl 1. n)
-  
-  (** val lnot : float -> float -> float **)
-  
-  let lnot a n =
-    coq_lxor a (ones 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
-
diff --git a/generator/tests/jsref/BinPos.ml b/generator/tests/jsref/BinPos.ml
deleted file mode 100644
index 6bd8cc3a1ab8439f4b7c4f65963dfe05332045f6..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/BinPos.ml
+++ /dev/null
@@ -1,1053 +0,0 @@
-open BinPosDef
-open Bool0
-open Datatypes
-open Peano
-
-(*
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-*)
-
-module Pos = 
- struct 
-  type t = float
-  
-  (* HACK *)
-  let is_even p =
-     float_eq (mod_float p 2.) 0.
-
-
-  (** val succ : float -> float **)
-  
-  let rec succ = (+.) 1.
-  
-  (** val add : float -> float -> float **)
-  
-  let rec add = (+.)
-  
-  (** val add_carry : float -> float -> float **)
-  
-  and add_carry x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (add_carry p q))
-        (fun q -> (fun p -> 2. *. p)
-        (add_carry p q))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        (succ p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 2. *. p)
-        (add_carry p q))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (add p q))
-        (fun _ -> (fun p -> 2. *. p)
-        (succ p))
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (succ q))
-        (fun q -> (fun p -> 2. *. p)
-        (succ q))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        1.)
-        y)
-      x
-  
-  (** val pred_double : float -> float **)
-  
-  let rec pred_double x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
-      p))
-      (fun p -> (fun p -> 1. +. (2. *. p))
-      (pred_double p))
-      (fun _ ->
-      1.)
-      x
-  
-  (** val pred : float -> float **)
-  
-  let pred = (fun x -> x -. 1.)
-  
-  (** val pred_N : float -> float **)
-  
-  let pred_N x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> ((fun p -> 2. *. p)
-      p))
-      (fun p ->
-      (pred_double p))
-      (fun _ ->
-      0.)
-      x
-  
-  type mask = Pos.mask =
-  | IsNul [@f]  (** Auto Generated Attributes **)
-  | IsPos  [@f label0] of float (** Auto Generated Attributes **)
-  | IsNeg [@f]  (** Auto Generated Attributes **)
-  
-  (** val mask_rect : 'a1 -> (float -> 'a1) -> 'a1 -> mask -> 'a1 **)
-  
-  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 m = match m with
-  | IsNul -> f
-  | IsPos x -> f0 x
-  | IsNeg -> f1
-  
-  (** val succ_double_mask : mask -> mask **)
-  
-  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 m = match m with
-  | IsNul -> IsNul
-  | IsPos p -> IsPos ((fun p -> 2. *. p) p)
-  | IsNeg -> IsNeg
-  
-  (** val double_pred_mask : float -> mask **)
-  
-  let double_pred_mask x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> IsPos ((fun p -> 2. *. p) ((fun p -> 2. *. p)
-      p)))
-      (fun p -> IsPos ((fun p -> 2. *. p)
-      (pred_double p)))
-      (fun _ ->
-      IsNul)
-      x
-  
-  (** val pred_mask : mask -> mask **)
-  
-  let pred_mask m = match m with
-  | IsNul -> IsNeg
-  | IsPos q ->
-    ((fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-       (fun p0 -> IsPos
-       (pred q))
-       (fun p0 -> IsPos
-       (pred q))
-       (fun _ ->
-       IsNul)
-       q)
-  | IsNeg -> IsNeg
-  
-  (** val sub_mask : float -> float -> mask **)
-  
-  let rec sub_mask x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        double_mask (sub_mask p q))
-        (fun q ->
-        succ_double_mask (sub_mask p q))
-        (fun _ -> IsPos ((fun p -> 2. *. p)
-        p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        succ_double_mask (sub_mask_carry p q))
-        (fun q ->
-        double_mask (sub_mask p q))
-        (fun _ -> IsPos
-        (pred_double p))
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p ->
-        IsNeg)
-        (fun p ->
-        IsNeg)
-        (fun _ ->
-        IsNul)
-        y)
-      x
-  
-  (** val sub_mask_carry : float -> float -> mask **)
-  
-  and sub_mask_carry x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        succ_double_mask (sub_mask_carry p q))
-        (fun q ->
-        double_mask (sub_mask p q))
-        (fun _ -> IsPos
-        (pred_double p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        double_mask (sub_mask_carry p q))
-        (fun q ->
-        succ_double_mask (sub_mask_carry p q))
-        (fun _ ->
-        double_pred_mask p)
-        y)
-      (fun _ ->
-      IsNeg)
-      x
-  
-  (** val sub : float -> float -> float **)
-  
-  let sub = (-.)
-  
-  (** val mul : float -> float -> float **)
-  
-  let rec mul = ( *. )
-  
-  (** val iter : float -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let rec iter n f x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun n' ->
-      f (iter n' f (iter n' f x)))
-      (fun n' ->
-      iter n' f (iter n' f x))
-      (fun _ ->
-      f x)
-      n
-  
-  (** val pow : float -> float -> float **)
-  
-  let pow x y =
-    iter y (mul x) 1.
-  
-  (** val square : float -> float **)
-  
-  let rec square p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
-      (add (square p0) p0)))
-      (fun p0 -> (fun p -> 2. *. p) ((fun p -> 2. *. p)
-      (square p0)))
-      (fun _ ->
-      1.)
-      p
-  
-  (** val div2 : float -> float **)
-  
-  let div2 p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      p0)
-      (fun p0 ->
-      p0)
-      (fun _ ->
-      1.)
-      p
-  
-  (** val div2_up : float -> float **)
-  
-  let div2_up p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      succ p0)
-      (fun p0 ->
-      p0)
-      (fun _ ->
-      1.)
-      p
-  
-  (** val size_nat : float -> int **)
-  
-  let rec size_nat p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 -> Pervasives.succ
-      (size_nat p0))
-      (fun p0 -> Pervasives.succ
-      (size_nat p0))
-      (fun _ -> Pervasives.succ
-      0)
-      p
-  
-  (** val size : float -> float **)
-  
-  let rec size p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      succ (size p0))
-      (fun p0 ->
-      succ (size p0))
-      (fun _ ->
-      1.)
-      p
-  
-  (** val compare_cont : float -> float -> comparison -> comparison **)
-  
-  let rec compare_cont = fun x y c -> if float_eq x y then c else if x<y then Lt else Gt
-  
-  (** val compare : float -> float -> comparison **)
-  
-  let compare = fun x y -> if float_eq x y then Eq else if x<y then Lt else Gt
-  
-  (** val min : float -> float -> float **)
-  
-  let min = min
-  
-  (** val max : float -> float -> float **)
-  
-  let max = max
-  
-  (** val eqb : float -> float -> bool **)
-  
-  let rec eqb p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        eqb p0 q0)
-        (fun p1 ->
-        false)
-        (fun _ ->
-        false)
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p1 ->
-        false)
-        (fun q0 ->
-        eqb p0 q0)
-        (fun _ ->
-        false)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        false)
-        (fun p0 ->
-        false)
-        (fun _ ->
-        true)
-        q)
-      p
-  
-  (** val leb : float -> float -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Eq -> true
-    | Lt -> true
-    | Gt -> false
-  
-  (** val ltb : float -> float -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Eq -> false
-    | Lt -> true
-    | Gt -> false
-  
-  (** val sqrtrem_step :
-      (float -> float) -> (float -> float) -> (float * mask) -> float * mask **)
-  
-  let sqrtrem_step f g p = 
-    let (s, y) = p in
-    (match y with
-     | IsNul ->
-       (((fun p -> 2. *. p) s),
-         (sub_mask (g (f 1.)) ((fun p -> 2. *. p) ((fun p -> 2. *. p) 1.))))
-     | IsPos r ->
-       let s' = (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p) s) in
-       let r' = g (f r) in
-       if leb s' r'
-       then (((fun p -> 1. +. (2. *. p)) s), (sub_mask r' s'))
-       else (((fun p -> 2. *. p) s), (IsPos r'))
-     | IsNeg ->
-       (((fun p -> 2. *. p) s),
-         (sub_mask (g (f 1.)) ((fun p -> 2. *. p) ((fun p -> 2. *. p) 1.)))))
-  
-  (** val sqrtrem : float -> float * mask **)
-  
-  let rec sqrtrem p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
-          (fun p -> 1. +. (2. *. p)) x) (sqrtrem p1))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 2. *. p) x) (fun x ->
-          (fun p -> 1. +. (2. *. p)) x) (sqrtrem p1))
-        (fun _ -> (1., (IsPos ((fun p -> 2. *. p)
-        1.))))
-        p0)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
-          (fun p -> 2. *. p) x) (sqrtrem p1))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 2. *. p) x) (fun x ->
-          (fun p -> 2. *. p) x) (sqrtrem p1))
-        (fun _ -> (1., (IsPos
-        1.)))
-        p0)
-      (fun _ -> (1.,
-      IsNul))
-      p
-  
-  (** val sqrt : float -> float **)
-  
-  let sqrt p =
-    fst (sqrtrem p)
-  
-  (** val gcdn : int -> float -> float -> float **)
-  
-  let rec gcdn n a b =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      1.)
-      (fun n0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun a' ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun b' ->
-          match compare a' b' with
-          | Eq -> a
-          | Lt -> gcdn n0 (sub b' a') a
-          | Gt -> gcdn n0 (sub a' b') b)
-          (fun b0 ->
-          gcdn n0 a b0)
-          (fun _ ->
-          1.)
-          b)
-        (fun a0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p ->
-          gcdn n0 a0 b)
-          (fun b0 -> (fun p -> 2. *. p)
-          (gcdn n0 a0 b0))
-          (fun _ ->
-          1.)
-          b)
-        (fun _ ->
-        1.)
-        a)
-      n
-  
-  (** val gcd : float -> float -> float **)
-  
-  let gcd a b =
-    gcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val ggcdn : int -> float -> float -> float * (float * float) **)
-  
-  let rec ggcdn n a b =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ -> (1., (a,
-      b)))
-      (fun n0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun a' ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun b' ->
-          match compare a' b' with
-          | Eq -> (a, (1., 1.))
-          | Lt ->
-            let (g, p) = ggcdn n0 (sub b' a') a in
-            let (ba, aa) = p in (g, (aa, (add aa ((fun p -> 2. *. p) ba))))
-          | Gt ->
-            let (g, p) = ggcdn n0 (sub a' b') b in
-            let (ab, bb) = p in (g, ((add bb ((fun p -> 2. *. p) ab)), bb)))
-          (fun b0 ->
-          let (g, p) = ggcdn n0 a b0 in
-          let (aa, bb) = p in (g, (aa, ((fun p -> 2. *. p) bb))))
-          (fun _ -> (1., (a,
-          1.)))
-          b)
-        (fun a0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p ->
-          let (g, p0) = ggcdn n0 a0 b in
-          let (aa, bb) = p0 in (g, (((fun p -> 2. *. p) aa), bb)))
-          (fun b0 ->
-          let (g, p) = ggcdn n0 a0 b0 in (((fun p -> 2. *. p) g), p))
-          (fun _ -> (1., (a,
-          1.)))
-          b)
-        (fun _ -> (1., (1.,
-        b)))
-        a)
-      n
-  
-  (** val ggcd : float -> float -> float * (float * float) **)
-  
-  let ggcd a b =
-    ggcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val coq_Nsucc_double : float -> float **)
-  
-  let coq_Nsucc_double x =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      1.)
-      (fun p -> ((fun p -> 1. +. (2. *. p))
-      p))
-      x
-  
-  (** val coq_Ndouble : float -> float **)
-  
-  let coq_Ndouble n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p -> ((fun p -> 2. *. p)
-      p))
-      n
-  
-  (** val coq_lor : float -> float -> float **)
-  
-  let rec coq_lor p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        (coq_lor p0 q0))
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        (coq_lor p0 q0))
-        (fun _ ->
-        p)
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        (coq_lor p0 q0))
-        (fun q0 -> (fun p -> 2. *. p)
-        (coq_lor p0 q0))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        p0)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        q)
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        q0)
-        (fun _ ->
-        q)
-        q)
-      p
-  
-  (** val coq_land : float -> float -> float **)
-  
-  let rec coq_land p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Nsucc_double (coq_land p0 q0))
-        (fun q0 ->
-        coq_Ndouble (coq_land p0 q0))
-        (fun _ ->
-        1.)
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (coq_land p0 q0))
-        (fun q0 ->
-        coq_Ndouble (coq_land p0 q0))
-        (fun _ ->
-        0.)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        1.)
-        (fun q0 ->
-        0.)
-        (fun _ ->
-        1.)
-        q)
-      p
-  
-  (** val ldiff : float -> float -> float **)
-  
-  let rec ldiff p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (ldiff p0 q0))
-        (fun q0 ->
-        coq_Nsucc_double (ldiff p0 q0))
-        (fun _ -> ((fun p -> 2. *. p)
-        p0))
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (ldiff p0 q0))
-        (fun q0 ->
-        coq_Ndouble (ldiff p0 q0))
-        (fun _ ->
-        p)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        0.)
-        (fun q0 ->
-        1.)
-        (fun _ ->
-        0.)
-        q)
-      p
-  
-  (** val coq_lxor : float -> float -> float **)
-  
-  let rec coq_lxor p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (coq_lxor p0 q0))
-        (fun q0 ->
-        coq_Nsucc_double (coq_lxor p0 q0))
-        (fun _ -> ((fun p -> 2. *. p)
-        p0))
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Nsucc_double (coq_lxor p0 q0))
-        (fun q0 ->
-        coq_Ndouble (coq_lxor p0 q0))
-        (fun _ -> ((fun p -> 1. +. (2. *. p))
-        p0))
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 -> ((fun p -> 2. *. p)
-        q0))
-        (fun q0 -> ((fun p -> 1. +. (2. *. p))
-        q0))
-        (fun _ ->
-        0.)
-        q)
-      p
-  
-  (** val shiftl_nat : float -> int -> float **)
-  
-  let shiftl_nat p n =
-    nat_iter n (fun x -> (fun p -> 2. *. p) x) p
-  
-  (** val shiftr_nat : float -> int -> float **)
-  
-  let shiftr_nat p n =
-    nat_iter n div2 p
-  
-  (** val shiftl : float -> float -> float **)
-  
-  let shiftl p n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      p)
-      (fun n0 ->
-      iter n0 (fun x -> (fun p -> 2. *. p) x) p)
-      n
-  
-  (** val shiftr : float -> float -> float **)
-  
-  let shiftr p n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      p)
-      (fun n0 ->
-      iter n0 div2 p)
-      n
-  
-  (** val testbit_nat : float -> int -> bool **)
-  
-  let rec testbit_nat p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 n ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        true)
-        (fun n' ->
-        testbit_nat p0 n')
-        n)
-      (fun p0 n ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        false)
-        (fun n' ->
-        testbit_nat p0 n')
-        n)
-      (fun _ n ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        true)
-        (fun n0 ->
-        false)
-        n)
-      p
-  
-  (** val testbit : float -> float -> bool **)
-  
-  let rec testbit p n =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        true)
-        (fun n0 ->
-        testbit p0 (pred_N n0))
-        n)
-      (fun p0 ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        false)
-        (fun n0 ->
-        testbit p0 (pred_N n0))
-        n)
-      (fun _ ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        true)
-        (fun p0 ->
-        false)
-        n)
-      p
-  
-  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> float -> 'a1 -> 'a1 **)
-  
-  let iter_op op =
-    let rec iter0 p a =
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        op a (iter0 p0 (op a a)))
-        (fun p0 ->
-        iter0 p0 (op a a))
-        (fun _ ->
-        a)
-        p
-    in iter0
-  
-  (** val to_nat : float -> int **)
-  
-  let to_nat x =
-    iter_op plus x (Pervasives.succ 0)
-  
-  (** val of_nat : int -> float **)
-  
-  let rec of_nat n =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      1.)
-      (fun x ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        1.)
-        (fun n0 ->
-        succ (of_nat x))
-        x)
-      n
-  
-  (** val of_succ_nat : int -> float **)
-  
-  let rec of_succ_nat n =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      1.)
-      (fun x ->
-      succ (of_succ_nat x))
-      n
-  
-  (** val eq_dec : float -> float -> bool **)
-  
-  let eq_dec x y =
-    let rec f p =
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 y0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p1 ->
-          if f p0 p1 then true else false)
-          (fun p1 ->
-          false)
-          (fun _ ->
-          false)
-          y0)
-        (fun p0 y0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p1 ->
-          false)
-          (fun p1 ->
-          if f p0 p1 then true else false)
-          (fun _ ->
-          false)
-          y0)
-        (fun _ y0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p0 ->
-          false)
-          (fun p0 ->
-          false)
-          (fun _ ->
-          true)
-          y0)
-        p
-    in f x y
-  
-  (** val peano_rect : 'a1 -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let rec peano_rect a f p =
-    let f2 =
-      peano_rect (f 1. a) (fun p0 x ->
-        f (succ ((fun p -> 2. *. p) p0)) (f ((fun p -> 2. *. p) p0) x))
-    in
-    ((fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-       (fun q ->
-       f ((fun p -> 2. *. p) q) (f2 q))
-       (fun q ->
-       f2 q)
-       (fun _ ->
-       a)
-       p)
-  
-  (** val peano_rec : 'a1 -> (float -> 'a1 -> 'a1) -> float -> 'a1 **)
-  
-  let peano_rec =
-    peano_rect
-  
-  type coq_PeanoView =
-  | PeanoOne [@f]  (** Auto Generated Attributes **)
-  | PeanoSucc  [@f label0, label1] of float * coq_PeanoView (** Auto Generated Attributes **)
-  
-  (** val coq_PeanoView_rect :
-      'a1 -> (float -> coq_PeanoView -> 'a1 -> 'a1) -> float -> coq_PeanoView
-      -> 'a1 **)
-  
-  let rec coq_PeanoView_rect f f0 p p' = match p' with
-    | PeanoOne -> f
-    | 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 rec coq_PeanoView_rec f f0 p p' = match p' with
-    | PeanoOne -> f
-    | 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 p' = match p' with
-  | PeanoOne -> PeanoSucc (1., PeanoOne)
-  | PeanoSucc (p0, q0) ->
-    PeanoSucc ((succ ((fun p -> 2. *. p) p0)), (PeanoSucc
-      (((fun p -> 2. *. p) p0), (peanoView_xO p0 q0))))
-  
-  (** val peanoView_xI : float -> coq_PeanoView -> coq_PeanoView **)
-  
-  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
-      (((fun p -> 1. +. (2. *. p)) p0), (peanoView_xI p0 q0))))
-  
-  (** val peanoView : float -> coq_PeanoView **)
-  
-  let rec peanoView p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      peanoView_xI p0 (peanoView p0))
-      (fun p0 ->
-      peanoView_xO p0 (peanoView p0))
-      (fun _ ->
-      PeanoOne)
-      p
-  
-  (** val coq_PeanoView_iter :
-      'a1 -> (float -> 'a1 -> 'a1) -> float -> coq_PeanoView -> 'a1 **)
-  
-  let rec coq_PeanoView_iter a f p p' = match p' with
-    | PeanoOne -> a
-    | 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 c' = match c' with
-  | Eq -> c
-  | Lt -> Lt
-  | Gt -> Gt
-  
-  (** val mask2cmp : mask -> comparison **)
-  
-  let mask2cmp m = match m with
-  | IsNul -> Eq
-  | IsPos p0 -> Gt
-  | IsNeg -> Lt
-  
-  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
diff --git a/generator/tests/jsref/BinPosDef.ml b/generator/tests/jsref/BinPosDef.ml
deleted file mode 100644
index 5ef3d33f53cdb9ac855d0ed4494ed7e89d072101..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/BinPosDef.ml
+++ /dev/null
@@ -1,929 +0,0 @@
-open Datatypes
-open Peano
-
-module Pos = 
- struct 
-  type t = float
-  
-
-  (* HACK *)
-  let is_even p =
-     float_eq (mod_float p 2.) 0.
-
-
-  (** val succ : float -> float **)
-  
-  let rec succ x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> (fun p -> 2. *. p)
-      (succ p))
-      (fun p -> (fun p -> 1. +. (2. *. p))
-      p)
-      (fun _ -> (fun p -> 2. *. p)
-      1.)
-      x
-  
-  (** val add : float -> float -> float **)
-  
-  let rec add x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 2. *. p)
-        (add_carry p q))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (add p q))
-        (fun _ -> (fun p -> 2. *. p)
-        (succ p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (add p q))
-        (fun q -> (fun p -> 2. *. p)
-        (add p q))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        p)
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 2. *. p)
-        (succ q))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        q)
-        (fun _ -> (fun p -> 2. *. p)
-        1.)
-        y)
-      x
-  
-  (** val add_carry : float -> float -> float **)
-  
-  and add_carry x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (add_carry p q))
-        (fun q -> (fun p -> 2. *. p)
-        (add_carry p q))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        (succ p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 2. *. p)
-        (add_carry p q))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (add p q))
-        (fun _ -> (fun p -> 2. *. p)
-        (succ p))
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q -> (fun p -> 1. +. (2. *. p))
-        (succ q))
-        (fun q -> (fun p -> 2. *. p)
-        (succ q))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        1.)
-        y)
-      x
-  
-  (** val pred_double : float -> float **)
-  
-  let rec pred_double x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
-      p))
-      (fun p -> (fun p -> 1. +. (2. *. p))
-      (pred_double p))
-      (fun _ ->
-      1.)
-      x
-  
-  (** val pred : float -> float **)
-  
-  let pred x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> (fun p -> 2. *. p)
-      p)
-      (fun p ->
-      pred_double p)
-      (fun _ ->
-      1.)
-      x
-  
-  (** val pred_N : float -> float **)
-  
-  let pred_N x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> ((fun p -> 2. *. p)
-      p))
-      (fun p ->
-      (pred_double p))
-      (fun _ ->
-      0.)
-      x
-  
-  type mask =
-  | IsNul [@f]  (** Auto Generated Attributes **)
-  | IsPos  [@f label0] of float (** Auto Generated Attributes **)
-  | IsNeg [@f]  (** Auto Generated Attributes **)
-  
-  (** val mask_rect : 'a1 -> (float -> 'a1) -> 'a1 -> mask -> 'a1 **)
-  
-  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 mask = match mask with
-  | IsNul -> f
-  | IsPos x -> f0 x
-  | IsNeg -> f1
-  
-  (** val succ_double_mask : mask -> mask **)
-  
-  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 m = match m with
-  | IsNul -> IsNul
-  | IsPos p -> IsPos ((fun p -> 2. *. p) p)
-  | IsNeg -> IsNeg
-  
-  (** val double_pred_mask : float -> mask **)
-  
-  let double_pred_mask x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p -> IsPos ((fun p -> 2. *. p) ((fun p -> 2. *. p)
-      p)))
-      (fun p -> IsPos ((fun p -> 2. *. p)
-      (pred_double p)))
-      (fun _ ->
-      IsNul)
-      x
-  
-  (** val pred_mask : mask -> mask **)
-  
-  let pred_mask m = match m with
-  | IsNul -> IsNeg
-  | IsPos q ->
-    ((fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-       (fun p0 -> IsPos
-       (pred q))
-       (fun p0 -> IsPos
-       (pred q))
-       (fun _ ->
-       IsNul)
-       q)
-  | IsNeg -> IsNeg
-  
-  (** val sub_mask : float -> float -> mask **)
-  
-  let rec sub_mask x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        double_mask (sub_mask p q))
-        (fun q ->
-        succ_double_mask (sub_mask p q))
-        (fun _ -> IsPos ((fun p -> 2. *. p)
-        p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        succ_double_mask (sub_mask_carry p q))
-        (fun q ->
-        double_mask (sub_mask p q))
-        (fun _ -> IsPos
-        (pred_double p))
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p ->
-        IsNeg)
-        (fun p ->
-        IsNeg)
-        (fun _ ->
-        IsNul)
-        y)
-      x
-  
-  (** val sub_mask_carry : float -> float -> mask **)
-  
-  and sub_mask_carry x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        succ_double_mask (sub_mask_carry p q))
-        (fun q ->
-        double_mask (sub_mask p q))
-        (fun _ -> IsPos
-        (pred_double p))
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        double_mask (sub_mask_carry p q))
-        (fun q ->
-        succ_double_mask (sub_mask_carry p q))
-        (fun _ ->
-        double_pred_mask p)
-        y)
-      (fun _ ->
-      IsNeg)
-      x
-  
-  (** val sub : float -> float -> float **)
-  
-  let sub x y =
-    match sub_mask x y with
-    | IsNul -> 1.
-    | IsPos z -> z
-    | IsNeg -> 1.
-  
-  (** val mul : float -> float -> float **)
-  
-  let rec mul x y =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      add y ((fun p -> 2. *. p) (mul p y)))
-      (fun p -> (fun p -> 2. *. p)
-      (mul p y))
-      (fun _ ->
-      y)
-      x
-  
-  (** val iter : float -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-  
-  let rec iter n f x =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun n' ->
-      f (iter n' f (iter n' f x)))
-      (fun n' ->
-      iter n' f (iter n' f x))
-      (fun _ ->
-      f x)
-      n
-  
-  (** val pow : float -> float -> float **)
-  
-  let pow x y =
-    iter y (mul x) 1.
-  
-  (** val square : float -> float **)
-  
-  let rec square p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 -> (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p)
-      (add (square p0) p0)))
-      (fun p0 -> (fun p -> 2. *. p) ((fun p -> 2. *. p)
-      (square p0)))
-      (fun _ ->
-      1.)
-      p
-  
-  (** val div2 : float -> float **)
-  
-  let div2 p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      p0)
-      (fun p0 ->
-      p0)
-      (fun _ ->
-      1.)
-      p
-  
-  (** val div2_up : float -> float **)
-  
-  let div2_up p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      succ p0)
-      (fun p0 ->
-      p0)
-      (fun _ ->
-      1.)
-      p
-  
-  (** val size_nat : float -> int **)
-  
-  let rec size_nat p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 -> Pervasives.succ
-      (size_nat p0))
-      (fun p0 -> Pervasives.succ
-      (size_nat p0))
-      (fun _ -> Pervasives.succ
-      0)
-      p
-  
-  (** val size : float -> float **)
-  
-  let rec size p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      succ (size p0))
-      (fun p0 ->
-      succ (size p0))
-      (fun _ ->
-      1.)
-      p
-  
-  (** val compare_cont : float -> float -> comparison -> comparison **)
-  
-  let rec compare_cont x y r =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        compare_cont p q r)
-        (fun q ->
-        compare_cont p q Gt)
-        (fun _ ->
-        Gt)
-        y)
-      (fun p ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        compare_cont p q Lt)
-        (fun q ->
-        compare_cont p q r)
-        (fun _ ->
-        Gt)
-        y)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q ->
-        Lt)
-        (fun q ->
-        Lt)
-        (fun _ ->
-        r)
-        y)
-      x
-  
-  (** val compare : float -> float -> comparison **)
-  
-  let compare x y =
-    compare_cont x y Eq
-  
-  (** val min : float -> float -> float **)
-  
-  let min p p' =
-    match compare p p' with
-    | Eq -> p
-    | Lt -> p
-    | Gt -> p'
-  
-  (** val max : float -> float -> float **)
-  
-  let max p p' =
-    match compare p p' with
-    | Eq -> p'
-    | Lt -> p'
-    | Gt -> p
-  
-  (** val eqb : float -> float -> bool **)
-  
-  let rec eqb p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        eqb p0 q0)
-        (fun p1 ->
-        false)
-        (fun _ ->
-        false)
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p1 ->
-        false)
-        (fun q0 ->
-        eqb p0 q0)
-        (fun _ ->
-        false)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        false)
-        (fun p0 ->
-        false)
-        (fun _ ->
-        true)
-        q)
-      p
-  
-  (** val leb : float -> float -> bool **)
-  
-  let leb x y =
-    match compare x y with
-    | Eq -> true
-    | Lt -> true
-    | Gt -> false
-  
-  (** val ltb : float -> float -> bool **)
-  
-  let ltb x y =
-    match compare x y with
-    | Eq -> false
-    | Lt -> true
-    | Gt -> false
-  
-  (** val sqrtrem_step :
-      (float -> float) -> (float -> float) -> (float * mask) -> float * mask **)
-  
-  let sqrtrem_step f g p =
-  let (s, y) = p in
-    (match y with
-     | IsNul ->
-       (((fun p -> 2. *. p) s),
-         (sub_mask (g (f 1.)) ((fun p -> 2. *. p) ((fun p -> 2. *. p) 1.))))
-     | IsPos r ->
-       let s' = (fun p -> 1. +. (2. *. p)) ((fun p -> 2. *. p) s) in
-       let r' = g (f r) in
-       if leb s' r'
-       then (((fun p -> 1. +. (2. *. p)) s), (sub_mask r' s'))
-       else (((fun p -> 2. *. p) s), (IsPos r'))
-     | IsNeg ->
-       (((fun p -> 2. *. p) s),
-         (sub_mask (g (f 1.)) ((fun p -> 2. *. p) ((fun p -> 2. *. p) 1.)))))
-  
-  (** val sqrtrem : float -> float * mask **)
-  
-  let rec sqrtrem p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
-          (fun p -> 1. +. (2. *. p)) x) (sqrtrem p1))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 2. *. p) x) (fun x ->
-          (fun p -> 1. +. (2. *. p)) x) (sqrtrem p1))
-        (fun _ -> (1., (IsPos ((fun p -> 2. *. p)
-        1.))))
-        p0)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 1. +. (2. *. p)) x) (fun x ->
-          (fun p -> 2. *. p) x) (sqrtrem p1))
-        (fun p1 ->
-        sqrtrem_step (fun x -> (fun p -> 2. *. p) x) (fun x ->
-          (fun p -> 2. *. p) x) (sqrtrem p1))
-        (fun _ -> (1., (IsPos
-        1.)))
-        p0)
-      (fun _ -> (1.,
-      IsNul))
-      p
-  
-  (** val sqrt : float -> float **)
-  
-  let sqrt p =
-    fst (sqrtrem p)
-  
-  (** val gcdn : int -> float -> float -> float **)
-  
-  let rec gcdn n a b =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      1.)
-      (fun n0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun a' ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun b' ->
-          match compare a' b' with
-          | Eq -> a
-          | Lt -> gcdn n0 (sub b' a') a
-          | Gt -> gcdn n0 (sub a' b') b)
-          (fun b0 ->
-          gcdn n0 a b0)
-          (fun _ ->
-          1.)
-          b)
-        (fun a0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p ->
-          gcdn n0 a0 b)
-          (fun b0 -> (fun p -> 2. *. p)
-          (gcdn n0 a0 b0))
-          (fun _ ->
-          1.)
-          b)
-        (fun _ ->
-        1.)
-        a)
-      n
-  
-  (** val gcd : float -> float -> float **)
-  
-  let gcd a b =
-    gcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val ggcdn : int -> float -> float -> float * (float * float) **)
-  
-  let rec ggcdn n a b =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ -> (1., (a,
-      b)))
-      (fun n0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun a' ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun b' ->
-          match compare a' b' with
-          | Eq -> (a, (1., 1.))
-          | Lt ->
-            let (g, p) = ggcdn n0 (sub b' a') a in
-            let (ba, aa) = p in (g, (aa, (add aa ((fun p -> 2. *. p) ba))))
-          | Gt ->
-            let (g, p) = ggcdn n0 (sub a' b') b in
-            let (ab, bb) = p in (g, ((add bb ((fun p -> 2. *. p) ab)), bb)))
-          (fun b0 ->
-          let (g, p) = ggcdn n0 a b0 in
-          let (aa, bb) = p in (g, (aa, ((fun p -> 2. *. p) bb))))
-          (fun _ -> (1., (a,
-          1.)))
-          b)
-        (fun a0 ->
-        (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-          (fun p ->
-          let (g, p0) = ggcdn n0 a0 b in
-          let (aa, bb) = p0 in (g, (((fun p -> 2. *. p) aa), bb)))
-          (fun b0 ->
-          let (g, p) = ggcdn n0 a0 b0 in (((fun p -> 2. *. p) g), p))
-          (fun _ -> (1., (a,
-          1.)))
-          b)
-        (fun _ -> (1., (1.,
-        b)))
-        a)
-      n
-  
-  (** val ggcd : float -> float -> float * (float * float) **)
-  
-  let ggcd a b =
-    ggcdn (plus (size_nat a) (size_nat b)) a b
-  
-  (** val coq_Nsucc_double : float -> float **)
-  
-  let coq_Nsucc_double x =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      1.)
-      (fun p -> ((fun p -> 1. +. (2. *. p))
-      p))
-      x
-  
-  (** val coq_Ndouble : float -> float **)
-  
-  let coq_Ndouble n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      0.)
-      (fun p -> ((fun p -> 2. *. p)
-      p))
-      n
-  
-  (** val coq_lor : float -> float -> float **)
-  
-  let rec coq_lor p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        (coq_lor p0 q0))
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        (coq_lor p0 q0))
-        (fun _ ->
-        p)
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        (coq_lor p0 q0))
-        (fun q0 -> (fun p -> 2. *. p)
-        (coq_lor p0 q0))
-        (fun _ -> (fun p -> 1. +. (2. *. p))
-        p0)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        q)
-        (fun q0 -> (fun p -> 1. +. (2. *. p))
-        q0)
-        (fun _ ->
-        q)
-        q)
-      p
-  
-  (** val coq_land : float -> float -> float **)
-  
-  let rec coq_land p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Nsucc_double (coq_land p0 q0))
-        (fun q0 ->
-        coq_Ndouble (coq_land p0 q0))
-        (fun _ ->
-        1.)
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (coq_land p0 q0))
-        (fun q0 ->
-        coq_Ndouble (coq_land p0 q0))
-        (fun _ ->
-        0.)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        1.)
-        (fun q0 ->
-        0.)
-        (fun _ ->
-        1.)
-        q)
-      p
-  
-  (** val ldiff : float -> float -> float **)
-  
-  let rec ldiff p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (ldiff p0 q0))
-        (fun q0 ->
-        coq_Nsucc_double (ldiff p0 q0))
-        (fun _ -> ((fun p -> 2. *. p)
-        p0))
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (ldiff p0 q0))
-        (fun q0 ->
-        coq_Ndouble (ldiff p0 q0))
-        (fun _ ->
-        p)
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        0.)
-        (fun q0 ->
-        1.)
-        (fun _ ->
-        0.)
-        q)
-      p
-  
-  (** val coq_lxor : float -> float -> float **)
-  
-  let rec coq_lxor p q =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Ndouble (coq_lxor p0 q0))
-        (fun q0 ->
-        coq_Nsucc_double (coq_lxor p0 q0))
-        (fun _ -> ((fun p -> 2. *. p)
-        p0))
-        q)
-      (fun p0 ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 ->
-        coq_Nsucc_double (coq_lxor p0 q0))
-        (fun q0 ->
-        coq_Ndouble (coq_lxor p0 q0))
-        (fun _ -> ((fun p -> 1. +. (2. *. p))
-        p0))
-        q)
-      (fun _ ->
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun q0 -> ((fun p -> 2. *. p)
-        q0))
-        (fun q0 -> ((fun p -> 1. +. (2. *. p))
-        q0))
-        (fun _ ->
-        0.)
-        q)
-      p
-  
-  (** val shiftl_nat : float -> int -> float **)
-  
-  let shiftl_nat p n =
-    nat_iter n (fun x -> (fun p -> 2. *. p) x) p
-  
-  (** val shiftr_nat : float -> int -> float **)
-  
-  let shiftr_nat p n =
-    nat_iter n div2 p
-  
-  (** val shiftl : float -> float -> float **)
-  
-  let shiftl p n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      p)
-      (fun n0 ->
-      iter n0 (fun x -> (fun p -> 2. *. p) x) p)
-      n
-  
-  (** val shiftr : float -> float -> float **)
-  
-  let shiftr p n =
-    (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-      (fun _ ->
-      p)
-      (fun n0 ->
-      iter n0 div2 p)
-      n
-  
-  (** val testbit_nat : float -> int -> bool **)
-  
-  let rec testbit_nat p =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 n ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        true)
-        (fun n' ->
-        testbit_nat p0 n')
-        n)
-      (fun p0 n ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        false)
-        (fun n' ->
-        testbit_nat p0 n')
-        n)
-      (fun _ n ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        true)
-        (fun n0 ->
-        false)
-        n)
-      p
-  
-  (** val testbit : float -> float -> bool **)
-  
-  let rec testbit p n =
-    (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-      (fun p0 ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        true)
-        (fun n0 ->
-        testbit p0 (pred_N n0))
-        n)
-      (fun p0 ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        false)
-        (fun n0 ->
-        testbit p0 (pred_N n0))
-        n)
-      (fun _ ->
-      (fun f0 fp n -> if float_eq n 0. then f0 () else fp n)
-        (fun _ ->
-        true)
-        (fun p0 ->
-        false)
-        n)
-      p
-  
-  (** val iter_op : ('a1 -> 'a1 -> 'a1) -> float -> 'a1 -> 'a1 **)
-  
-  let iter_op op =
-    let rec iter0 p a =
-      (fun f2p1 f2p f1 p ->
-if p <= 1. then f1 () else if is_even p then f2p (floor (p /. 2.)) else f2p1 (floor (p /. 2.)))
-        (fun p0 ->
-        op a (iter0 p0 (op a a)))
-        (fun p0 ->
-        iter0 p0 (op a a))
-        (fun _ ->
-        a)
-        p
-    in iter0
-  
-  (** val to_nat : float -> int **)
-  
-  let to_nat x =
-    iter_op plus x (Pervasives.succ 0)
-  
-  (** val of_nat : int -> float **)
-  
-  let rec of_nat n =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      1.)
-      (fun x ->
-      (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-        (fun _ ->
-        1.)
-        (fun n0 ->
-        succ (of_nat x))
-        x)
-      n
-  
-  (** val of_succ_nat : int -> float **)
-  
-  let rec of_succ_nat n =
-    (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-      (fun _ ->
-      1.)
-      (fun x ->
-      succ (of_succ_nat x))
-      n
- end
-
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index 8ed80b09654bedefd400be6809ea02f9d9704a17..de739b02746b3f80cc859290642a188254dcd6bc 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -4,7 +4,6 @@ open JsNumber
 open JsSyntax
 open JsSyntaxAux
 open LibList
-open LibNat
 open LibOption
 open LibString
 open List0
@@ -354,7 +353,7 @@ let decl_env_record_rem ed x =
     state -> env_loc -> prop_name -> mutability -> value -> state **)
 
 let env_record_write_decl_env s l x mu v =
-  match Heap.read nat_comparable s.state_env_record_heap l with
+  match Heap.read nat_eq s.state_env_record_heap l with
   | Coq_env_record_decl ed ->
     let env' = decl_env_record_write ed x mu v in
     env_record_write s l (Coq_env_record_decl env')
@@ -559,7 +558,7 @@ let rec elision_head_count _foo_ = match _foo_ with
 | o :: ol' ->
   (match o with
    | Some t -> 0
-   | None -> Pervasives.succ (elision_head_count ol'))
+   | None -> 1 + (elision_head_count ol'))
 
 (** val elision_head_remove : 'a1 option list -> 'a1 option list **)
 
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index ff87f899b7d8d5d9e181b88c111b8c8813e52b37..141191b99bd73eaca20d2da6a13f0c6fdb0ab2f4 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -4,7 +4,6 @@ open JsNumber
 open JsSyntax
 open JsSyntaxAux
 open LibList
-open LibNat
 open LibOption
 open LibReflect
 open LibString
@@ -207,7 +206,7 @@ let object_binds_pickable_option s l =
     state -> env_loc -> env_record coq_Pickable_option **)
 
 let env_record_binds_pickable_option s l =
-  Heap.read_option nat_comparable s.state_env_record_heap l
+  Heap.read_option nat_eq s.state_env_record_heap l
 
 (** val decl_env_record_pickable_option :
     decl_env_record -> prop_name -> (mutability * value) coq_Pickable_option **)
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index 56d2c226d2421abc9e1066bd7180e521a7f62ca7..5b5d8c301578ce2e81c1c454d072cec04626aa3b 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -3,7 +3,6 @@ open JsNumber
 open JsPreliminary
 open JsSyntax
 open JsSyntaxAux
-open LibInt
 
 (** Val prop_attributes_for_global_object : value -> attributes_data **)
 
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 1b1fcb3da50dd3e9292911057a6d633bcb7a6242..98d32d8beaead71c818140e60a772acd770e0ece 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -1,4 +1,3 @@
-open BinInt
 open Datatypes
 open JsCommon
 open JsCommonAux
@@ -11,9 +10,7 @@ open JsSyntaxAux
 open JsSyntaxInfos
 open LibBool
 open LibFunc
-open LibInt
 open LibList
-open LibNat
 open LibOption
 open LibProd
 open LibReflect
@@ -2225,7 +2222,7 @@ let run_construct_prealloc runs0 s c b args =
                   attributes_data_configurable = false }))) (fun s0 ->
               res_ter s0 (res_val (Coq_value_object l)))) (fun follow ->
             let_binding (LibList.length args) (fun arg_len ->
-              if nat_comparable arg_len (Pervasives.succ 0)
+              if nat_eq arg_len 1
               then let_binding (get_arg 0 args) (fun v ->
                      match v with
                      | Coq_value_prim p0 ->
@@ -2360,7 +2357,7 @@ let run_construct_prealloc runs0 s c b args =
                     (Coq_attributes_data_of lenDesc))) (fun s' ->
                 res_ter s' (res_val (Coq_value_object l)))))) (fun follow ->
           let_binding (LibList.length args) (fun arg_len ->
-            if nat_comparable arg_len 0
+            if nat_eq arg_len 0
             then follow s ""
             else let_binding (get_arg 0 args) (fun arg ->
                    if_string (to_string runs0 s c arg) (fun s0 s1 ->
@@ -2673,7 +2670,7 @@ let rec binding_inst_function_decls runs0 s c l fds str bconfig =
                 if_bool (env_record_has_binding runs0 s1 c l fname)
                   (fun s2 has ->
                   if has
-                  then if nat_comparable l env_loc_global_env_record
+                  then if nat_eq l env_loc_global_env_record
                        then if_spec
                               (run_object_get_prop runs0 s2 c
                                 (Coq_object_loc_prealloc Coq_prealloc_global)
@@ -5377,7 +5374,7 @@ let run_call_prealloc runs0 s c b vthis args =
       match v with
       | Coq_value_prim p -> run_error s Coq_native_error_type
       | Coq_value_object l ->
-        if_string (to_string runs0 s c (get_arg (Pervasives.succ 0) args))
+        if_string (to_string runs0 s c (get_arg 1 args))
           (fun s1 x ->
           if_spec (runs0.runs_type_object_get_own_prop s1 c l x) (fun s2 d ->
             from_prop_descriptor runs0 s2 c d)))
@@ -5399,8 +5396,8 @@ let run_call_prealloc runs0 s c b vthis args =
           (" not yet implemented")))
   | Coq_prealloc_object_define_prop ->
     let_binding (get_arg 0 args) (fun o ->
-      let_binding (get_arg (Pervasives.succ 0) args) (fun p ->
-        let_binding (get_arg (Pervasives.succ (Pervasives.succ 0)) args)
+      let_binding (get_arg 1 args) (fun p ->
+        let_binding (get_arg 2 args)
           (fun attr ->
           match o with
           | Coq_value_prim p0 -> run_error s Coq_native_error_type
@@ -5580,7 +5577,7 @@ let run_call_prealloc runs0 s c b vthis args =
     else run_error s Coq_native_error_type
   | Coq_prealloc_function_proto_apply ->
     let_binding (get_arg 0 args) (fun thisArg ->
-      let_binding (get_arg (Pervasives.succ 0) args) (fun argArray ->
+      let_binding (get_arg 1 args) (fun argArray ->
         if is_callable_dec s vthis
         then (match vthis with
               | Coq_value_prim p ->
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index 03f3be522792ba0175eb4ae407bf825d0911fdaa..8dc8963bab0e14f66821d053a058b26171241ff1 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -1,6 +1,8 @@
 open Fappli_IEEE_bits
 open LibReflect
 
+let nat_eq = int_eq
+
 type number = binary64
 
 (** val nan : number **)
diff --git a/generator/tests/jsref/JsSyntaxAux.ml b/generator/tests/jsref/JsSyntaxAux.ml
index dbdc9eee7396c118f8b44ba70b540fb766a0e1f8..079c0da83d69bfffef0fda0e4f6ddbc91e8d6465 100644
--- a/generator/tests/jsref/JsSyntaxAux.ml
+++ b/generator/tests/jsref/JsSyntaxAux.ml
@@ -1,7 +1,6 @@
 open JsNumber
 open JsSyntax
 open LibList
-open LibNat
 open LibReflect
 open LibString
 
@@ -395,7 +394,7 @@ let object_loc_compare l1 l2 =
   match l1 with
   | Coq_object_loc_normal ln1 ->
     (match l2 with
-     | Coq_object_loc_normal ln2 -> nat_comparable ln1 ln2
+     | Coq_object_loc_normal ln2 -> nat_eq ln1 ln2
      | Coq_object_loc_prealloc p -> false)
   | Coq_object_loc_prealloc bl1 ->
     (match l2 with
@@ -515,7 +514,7 @@ let ref_base_type_compare rb1 rb2 =
   | Coq_ref_base_type_env_loc l1 ->
     (match rb2 with
      | Coq_ref_base_type_value v -> false
-     | Coq_ref_base_type_env_loc l2 -> nat_comparable l1 l2)
+     | Coq_ref_base_type_env_loc l2 -> nat_eq l1 l2)
 
 (** val ref_base_type_comparable : ref_base_type coq_Comparable **)
 
diff --git a/generator/tests/jsref/LibInt.ml b/generator/tests/jsref/LibInt.ml
deleted file mode 100644
index 4688e5ba6febf814910bddc5d981cb2aaf269621..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/LibInt.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-open BinInt
-open Datatypes
-open LibReflect
-
diff --git a/generator/tests/jsref/LibList.ml b/generator/tests/jsref/LibList.ml
index aafdc80cd3c6f56b4839a814ac95ff35bb1a1f22..c72c1770dc4452f75877c6375be9038cc38e7eef 100644
--- a/generator/tests/jsref/LibList.ml
+++ b/generator/tests/jsref/LibList.ml
@@ -48,7 +48,7 @@ let rev l =
 (** val length : 'a1 list -> int **)
 
 let length l =
-  fold_right (fun x acc -> plus (Pervasives.succ 0) acc) 0 l
+  fold_right (fun x acc -> plus 1 acc) 0 l
 
 (** val take_drop_last : 'a1 list -> 'a1 list * 'a1 **)
 
diff --git a/generator/tests/jsref/LibNat.ml b/generator/tests/jsref/LibNat.ml
deleted file mode 100644
index 96922ec018d493513d89367c1654935b32c70e44..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/LibNat.ml
+++ /dev/null
@@ -1,27 +0,0 @@
-open LibReflect
-
-(** val nat_compare : int -> int -> bool **)
-
-let rec nat_compare x y =
-  (fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
-    (fun _ ->
-    (fun fO fS n -> if int_eq  n 0 then fO () else fS (n-1))
-      (fun _ ->
-      true)
-      (fun n ->
-      false)
-      y)
-    (fun x' ->
-    (fun fO fS n -> if int_eq  n 0 then fO () else fS (n-1))
-      (fun _ ->
-      false)
-      (fun y' ->
-      nat_compare x' y')
-      y)
-    x
-
-(** val nat_comparable : int coq_Comparable **)
-
-let nat_comparable x y =
-  nat_compare x y
-
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index 74fe4256e0e958ab6330f4231cdfdd5cf86e2878..f811d694b29789a731f51a983931d3378412531b 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -1,9 +1,11 @@
-open BinInt
 open Datatypes
 open Heap
 open LibReflect
 open String0
 
+
+
+
 (** val option_case : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 
 let option_case d f o = match o with
diff --git a/generator/tests/jsref/String0.ml b/generator/tests/jsref/String0.ml
index b638ef0eeb8cda3ff6555140c3bc8622d78cd304..ad269fb174ddc83d7bf7bb35bd733f50d477b774 100644
--- a/generator/tests/jsref/String0.ml
+++ b/generator/tests/jsref/String0.ml
@@ -32,7 +32,7 @@ let rec append s1 s2 =
 
 let rec length l = match l with
 | [] -> 0
-| c::s' -> Pervasives.succ (length s')
+| c::s' -> 1 + (length s')
 
 (** val substring : int -> int -> string -> string **)