diff --git a/driver.html b/driver.html
index de797b885ab0d99a47ea0f1b1c145dae78359713..8c337447f71dd6f6fda4230f5f8dd724af6cd23e 100644
--- a/driver.html
+++ b/driver.html
@@ -23,6 +23,7 @@
 <script src="https://cdn.rawgit.com/jquery/esprima/1.2/esprima.js"></script>
 <script type = "text/javascript" src="esprima-to-ast.js"></script>
 <script type = "text/javascript" src="source-driver.js"></script>
+
 <!-- <script src="interp-poc.js"></script> -->
 
 <!-- <style> -->
@@ -85,56 +86,58 @@
 <h2>Mini-ML Interpreter</h2>
 
 
-<!-- <div class='source_div'> -->
-
-<!-- <table id='main_table'><tr> -->
-<!-- <td> -->
-<!--    <textarea id='source_code' class='source' rows='6' cols='60'>source code here</textarea> -->
-<!-- </td> -->
-<!-- <td width='600'> -->
-<!--    <div class="scroll-pane" style="height: 10em"> -->
-<!--    <div id='disp_env'>ctx here</div> -->
-<!--    </div> -->
-<!-- </td> -->
-<!-- </tr></table> -->
-<!-- </div> -->
-
-
-
-<!-- <br/> -->
-<!-- <div> -->
-<!-- <input type="button" id="button_run" value="RUN" /> -->
-<!-- Navigation: -->
-<!-- <input type="textbox" id='navigation_step' style="width:3em" value="0"/> -->
-<!-- / <span id="navigation_total"></span> -->
-<!-- <input type="button" id='button_reset' value="Reset" /> -->
-<!-- <input type="button" id='button_prev' value="Prev" /> -->
-<!-- <input type="button" id='button_next' value="Next" /> -->
-<!-- Reach condition: -->
-<!-- <input type="textbox" id='text_condition' style="width:30em" /> -->
-<!-- <input type="button" id='button_reach' value="Reach" /> -->
-<!-- <span id="reach_output"></span> -->
-<!-- </div> -->
-
-<!-- <div id="action_output"></div> -->
-<!-- <br/> -->
-
-<!-- <div class='source_div'> -->
-
-<!-- <table id='main_table'><tr> -->
-<!-- <td> -->
-<!--    <div id='file_list'></div> -->
-<!--    <textarea id='interpreter_code' class='source' rows='20' cols='60'></textarea> -->
-<!-- </td> -->
-<!-- <td width='600'> -->
-<!--    <div id='disp_infos'></div> -->
-<!--    <div id='disp_ctx'>ctx here</div> -->
-<!-- </td> -->
-<!-- </tr></table> -->
-<!-- </div> -->
-
-
-<!-- <script src="navig-poc.js"></script> -->
+<div class='source_div'>
+
+<table id='main_table'><tr>
+<td>
+   <textarea id='source_code' class='source' rows='6' cols='60'>source code here</textarea>
+</td>
+<td width='600'>
+   <div class="scroll-pane" style="height: 10em">
+   <div id='disp_env'>ctx here</div>
+   </div>
+</td>
+</tr></table>
+</div>
+
+
+
+<br/>
+<div>
+<input type="button" id="button_run" value="RUN" />
+Navigation:
+<input type="textbox" id='navigation_step' style="width:3em" value="0"/>
+/ <span id="navigation_total"></span>
+<input type="button" id='button_reset' value="Reset" />
+<input type="button" id='button_prev' value="Prev" />
+<input type="button" id='button_next' value="Next" />
+Reach condition:
+<input type="textbox" id='text_condition' style="width:30em" />
+<input type="button" id='button_reach' value="Reach" />
+<span id="reach_output"></span>
+</div>
+
+<div id="action_output"></div>
+<br/>
+
+<div class='source_div'>
+
+<table id='main_table'><tr>
+<td>
+   <div id='file_list'></div>
+   <textarea id='interpreter_code' class='source' rows='20' cols='60'></textarea>
+</td>
+<td width='600'>
+   <div id='disp_infos'></div>
+   <div id='disp_ctx'>ctx here</div>
+</td>
+</tr></table>
+</div>
+
+<script src="generator/tests/jsref/lineof.js"></script> 
+<script src="generator/tests/jsref/assembly.js"></script> 
+<script src="navig-driver.js"></script> 
+
 
 <!-- <\!-- -->
 <!-- <script language="javascript"> -->
diff --git a/generator/Makefile b/generator/Makefile
index e41fb31e73690a0fb0b65bd3b8b9b4cafe81f554..7c8d1fec7bcb78ab8d3655bc50ede155b6f4b29a 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -110,6 +110,10 @@ $(JSREF_PATH)/assembly.js: assembly.byte $(JSREF_ML:.ml=.log.js) $(JSREF_ML:.ml=
 	./assembly.byte -o $@ -stdlib $(STDLIB_DIR)/stdlib.js $(JSREF_ML:.ml=)
 
 
+# maybe useful
+
+tests/jsref/%.log.js: tests/jsref/%.ml 
+
 
 #####################################################################
 # Short targets
@@ -136,8 +140,9 @@ tests: $(TESTS_ML:.ml=.log.js) $(TESTS_ML:.ml=.token.js)
 
 DIRTY_EXTS := cmi,token.js,log.js,unlog.js,d,ml.d,mli.d
 
-clean_lineof:
+clean_genjs:
 	rm -f $(JSREF_PATH)/lineof.js
+	rm -f $(JSREF_PATH)/assembly.js
 
 clean_tests:
 	bash -c "rm -f $(TESTS_DIR)/*.{$(DIRTY_EXTS)}"
@@ -146,7 +151,7 @@ clean_tests:
 clean_stdlib:
 	rm -f $(STDLIB_DIR)/*.cmi
 
-clean: clean_lineof clean_tests clean_stdlib
+clean: clean_genjs clean_tests clean_stdlib
 	rm -rf _build
 	rm -f *.native *.byte
 
diff --git a/generator/TODO b/generator/TODO
index 1fb4388d2f79bbc4a60ba23d1c03724f90d82f63..a6abd71e4f26b7adcacfc18686c41cd17cccf158 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -1,4 +1,14 @@
 
+
+- reactivate
+	  default: throw "No matching case for switch";
+  by having js_of_pattern return an additional boolean indicating
+  whether there was a default case or not.
+	
+- optimize the lineof file to generate code that, at initialization
+  fills in an array with brute data, and a function that performs
+  look ups in the array to get the output
+
 - update the code that translates esprima syntax to recognize
   "use strict" directives, which come as first statement of
   a body, in hte form of a raw expression of raw type "use script".
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index 14601c49b4dabd5e0201dcf327cd6524c96b03f9..8acb5ff01dc79788e1b407ede20bccae9f07c6c6 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -142,7 +142,9 @@ let ppf_match value cases const =
     | Mode_cmi -> assert false
     | Mode_unlogged -> cases
     | Mode_line_token
-    | Mode_logged -> cases ^ "@,default: throw \"No matching case for switch\";"
+    | Mode_logged -> cases 
+      (* TODO: put back if there is not already a default case:
+          ^ "@,default: throw \"No matching case for switch\";" *)
     in
   let s = Printf.sprintf "switch (%s%s) {@;<1 2>@[<v 0>%s@]@,}@,"
     value cons_fld cases
@@ -163,7 +165,7 @@ let ppf_array values =
 let ppf_tuple = ppf_array
 
 let ppf_ifthen cond iftrue =
-  Printf.sprintf "(function () {@;<1 2>@[<v 2>@,if (%s) {@,return  %s;@,}@]@,})()"
+  Printf.sprintf "(function () {@;<1 2>@[<v 2>@,if (%s) {@,return %s;@,}@]@,})()"
                  cond iftrue
 
 let ppf_ifthenelse cond iftrue iffalse =
@@ -212,7 +214,7 @@ let ppf_cstrs styp cstr_name rest =
     | Mode_line_token
     | Mode_logged -> Printf.sprintf "type: \"%s\", " styp
     in
-  Printf.sprintf "@[<v 2>{%stag: \"%s\"%s %s}@]"
+  Printf.sprintf "{@[<v 2>%stag: \"%s\"%s %s@]}" (* TODO: cleanup *)
     styp_full cstr_name comma rest
 
 let ppf_cstrs_fct cstr_fullname args =
@@ -220,7 +222,7 @@ let ppf_cstrs_fct cstr_fullname args =
 
 let ppf_record llde =
   let rec aux acc = function
-    | []               -> Printf.sprintf "@[<v 2>{@;<1 2>%s@]@,}" acc
+    | []               -> Printf.sprintf "{@[<v 0>%s@]@,}" (*"@[<v 2>{@;<1 2>%s@]@,}"*) (* TODO: cleanup *) acc
     | (lbl, exp) :: [] -> aux (acc ^ Printf.sprintf "%s: %s" lbl exp) []
     | (lbl, exp) :: xs -> aux (acc ^ Printf.sprintf "%s: %s,@," lbl exp) xs
   in aux "" llde
@@ -353,7 +355,7 @@ let generate_logged_return ctx sbody =
      Printf.sprintf "%sreturn %s; %s" token_start sbody token_stop
   | Mode_logged ->
     let id = id_fresh "_return_" in
-    Printf.sprintf "var %s = %s;@,log_event(%s, ctx_push(%s, {\"return_value\", %s}), \"return\");@,return %s; "
+    Printf.sprintf "var %s = %s;@,log_event(%s, ctx_push(%s, [{key: \"return_value\", value: %s}]), \"return\");@,return %s; "
       id sbody token_lineof ctx id id
   | Mode_unlogged -> 
      Printf.sprintf "return %s; " sbody
@@ -676,6 +678,7 @@ and js_of_expression ctx dest e =
   | Texp_construct (p, cd, el) ->
     let cstr_fullname = string_of_longident p.txt in
     let cstr_name = cd.cstr_name in
+    let cstr_fullname = if cstr_fullname = "::" then "mk_cons" else cstr_fullname in  (* TODO: clean up this hack *)
     (*let styp = string_of_type_exp e.exp_type in*)
     let sexp =
       if is_sbool cstr_name then cstr_name else
@@ -698,7 +701,10 @@ and js_of_expression ctx dest e =
     (* ppf_while (js_of_expression cd) (js_of_expression body) *)
   | Texp_for        (id, _, st, ed, fl, body) -> out_of_scope loc "for"
     (* ppf_for (ppf_ident id) (js_of_expression st) (js_of_expression ed) fl (js_of_expression body) *)
-  | Texp_record     (llde,_)          -> ppf_record (List.map (fun (_, lbl, exp) -> (lbl.lbl_name, inline_of_wrap exp)) llde)
+  | Texp_record     (llde,_)          -> 
+      let sexp = ppf_record (List.map (fun (_, lbl, exp) -> (lbl.lbl_name, inline_of_wrap exp)) llde) in
+      apply_dest ctx dest sexp
+
   | Texp_field      (exp, _, lbl)     -> ppf_field_access (inline_of_wrap exp) lbl.lbl_name
   | Texp_assert      e                -> 
       let sexp = inline_of_wrap e in
@@ -753,7 +759,7 @@ and js_of_expression ctx dest e =
 and js_of_constant = function
   | Const_int       n     -> string_of_int n
   | Const_char      c     -> String.make 1 c
-  | Const_string   (s, _) -> "\"" ^ s ^ "\""
+  | Const_string   (s, _) -> "\"" ^ (String.escaped (String.escaped s)) ^ "\"" (* Warning: 2 levels of printf *)
   | Const_float     f     -> f
   | Const_int32     n     -> Int32.to_string n
   | Const_int64     n     -> Int64.to_string n
@@ -768,6 +774,7 @@ and js_of_longident loc =
   | "~-." -> "-"
   | "/."  -> "/"
   | "="   -> "=="
+  | "^"   -> "+" (* !!TODO: we want to claim ability to type our sublanguage, so we should not use this *)
   | res   -> ppf_ident_name res
 
 and is_primitive_comparison e =
diff --git a/generator/stdlib_ml/stdlib.js b/generator/stdlib_ml/stdlib.js
index 5ff1b68415011586d8d38d085e431a9185289457..e983ddaa02795d2feb6e504ee8e50117c725f7f7 100644
--- a/generator/stdlib_ml/stdlib.js
+++ b/generator/stdlib_ml/stdlib.js
@@ -1,3 +1,12 @@
+
+var mk_nil = function() {
+   return { type: "list", tag: "[]" };
+};
+
+var mk_cons = function(head, tail) {
+   return { type: "list", tag: "::", head: head, tail: tail };
+};
+
 var add = function (a, b) { return a + b }
 var sub = function (a, b) { return a - b }
 var mul = function (a, b) { return a * b }
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index eadaf32764237972d19075d6107f4c72ac89504a..44ff432f627c3105bf7233cc72d4025dc6e2f14a 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -62,11 +62,29 @@ val ( >= ) : float -> float -> bool
 
 val bool_eq : bool -> bool -> bool
 val int_eq : int -> int -> bool
+val int_lt : int -> int -> bool
 val int_ge : int -> int -> bool
 val string_eq : string -> string -> bool
 val float_eq : float -> float -> bool
+val float_lt : float -> float -> bool
+val float_le : float -> float -> bool
 val float_compare : float -> float -> int
 
+val string_concat : string -> string -> string
+
+
+val float_neg : float -> float (* ~-.*)
+
+val lt_bool : float -> float -> bool (*   (<) *)
+val add : float -> float -> float (*  (+.) *)
+val sub : float -> float -> float (*  (-.) *)
+val mult : float -> float -> float (*  ( *. ) *)
+val div : float -> float -> float (*  (/.) *)
+val fmod : float -> float -> float (*  mod_float *)
+val float_exp : float -> float -> float (* ( ** ) *)
+
+
+
 val ( && ) : bool -> bool -> bool
 val not : bool -> bool
 val stuck : string -> 'a
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index 141191b99bd73eaca20d2da6a13f0c6fdb0ab2f4..c8a5ef19de69a061ed0daf5d25e04131366432d7 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -376,10 +376,10 @@ let attributes_change_accessor_on_non_configurable_dec aa desc =
 let run_function_get_error_case s x = function
 | Coq_value_prim w -> false
 | Coq_value_object l ->
-  (&&)
     (if string_comparable x ("caller")
      then true
      else false)
+  &&
     (option_case false (fun o ->
       option_case false (fun bd -> funcbody_is_strict bd) o.object_code_)
       (object_binds_pickable_option s l))
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 98d32d8beaead71c818140e60a772acd770e0ece..6b81d97023732c61ada2ac295650a04cd19193fd 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -336,14 +336,14 @@ let object_get_builtin runs0 s c b vthis l x =
                | Coq_prim_number n -> Coq_result_impossible
                | Coq_prim_string s2 -> Coq_result_impossible)
             | Coq_value_object lf -> runs0.runs_type_call s1 c lf vthis []))))
-    (fun default ->
+    (fun def ->
     let_binding (fun s0 ->
-      if_value (default s0 l) (fun s' v ->
+      if_value (def s0 l) (fun s' v ->
         if spec_function_get_error_case_dec s' x v
         then run_error s' Coq_native_error_type
         else res_ter s' (res_val v))) (fun function0 ->
       match b with
-      | Coq_builtin_get_default -> default s l
+      | Coq_builtin_get_default -> def s l
       | Coq_builtin_get_function -> function0 s
       | Coq_builtin_get_args_obj ->
         if_some (run_object_method object_parameter_map_ s l) (fun lmapo ->
@@ -627,7 +627,7 @@ let object_can_put runs0 s c l x =
     descriptor -> bool -> bool -> (state -> prop_name -> descriptor ->
     strictness_flag -> __ specres) -> result **)
 
-let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc newWritable throw def =
+let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc newWritable throwcont def =
   if lt_int_decidable newLen oldLen
   then let_binding (oldLen -. 1.) (fun oldLen' ->
          if_string
@@ -647,10 +647,10 @@ let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc n
                       if_bool
                         (def s1 ("length")
                           newLenDesc1 false) (fun s2 x ->
-                        out_error_or_cst s2 throw Coq_native_error_type
+                        out_error_or_cst s2 throwcont Coq_native_error_type
                           (Coq_value_prim (Coq_prim_bool false)))))
              else runs0.runs_type_object_define_own_prop_array_loop s1 c l
-                    newLen oldLen' newLenDesc newWritable throw def)))
+                    newLen oldLen' newLenDesc newWritable throwcont def)))
   else if not_decidable (bool_decidable newWritable)
        then def s ("length")
               { descriptor_value = None; descriptor_writable = (Some false);
@@ -663,11 +663,11 @@ let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc n
     runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
     descriptor -> strictness_flag -> result **)
 
-let object_define_own_prop runs0 s c l x desc throw =
-  let_binding (fun s0 throw0 ->
-    out_error_or_cst s0 throw0 Coq_native_error_type (Coq_value_prim
+let object_define_own_prop runs0 s c l x desc throwcont =
+  let_binding (fun s0 throwcont0 ->
+    out_error_or_cst s0 throwcont0 Coq_native_error_type (Coq_value_prim
       (Coq_prim_bool false))) (fun reject ->
-    let_binding (fun s0 x0 desc0 throw0 ->
+    let_binding (fun s0 x0 desc0 throwcont0 ->
       if_spec (runs0.runs_type_object_get_own_prop s0 c l x0) (fun s1 d ->
         if_some (run_object_method object_extensible_ s1 l) (fun ext ->
           match d with
@@ -686,7 +686,7 @@ let object_define_own_prop runs0 s c l x desc throw =
                        (fun p -> Heap.write p x0 a)) (fun s2 ->
                      res_ter s2
                        (res_val (Coq_value_prim (Coq_prim_bool true)))))
-            else reject s1 throw0
+            else reject s1 throwcont0
           | Coq_full_descriptor_some a ->
             let_binding (fun s2 a0 ->
               let a' = attributes_update a0 desc0 in
@@ -699,7 +699,7 @@ let object_define_own_prop runs0 s c l x desc throw =
               then res_ter s1 (res_val (Coq_value_prim (Coq_prim_bool true)))
               else if attributes_change_enumerable_on_non_configurable_dec a
                         desc0
-                   then reject s1 throw0
+                   then reject s1 throwcont0
                    else if descriptor_is_generic_dec desc0
                         then object_define_own_prop_write s1 a
                         else if not_decidable
@@ -722,14 +722,14 @@ let object_define_own_prop runs0 s c l x desc throw =
                                              s1 l (fun p ->
                                              Heap.write p x0 a')) (fun s2 ->
                                            object_define_own_prop_write s2 a'))
-                                  else reject s1 throw0
+                                  else reject s1 throwcont0
                              else if and_decidable (attributes_is_data_dec a)
                                        (descriptor_is_data_dec desc0)
                                   then (match a with
                                         | Coq_attributes_data_of ad ->
                                           if attributes_change_data_on_non_configurable_dec
                                                ad desc0
-                                          then reject s1 throw0
+                                          then reject s1 throwcont0
                                           else object_define_own_prop_write
                                                  s1 a
                                         | Coq_attributes_accessor_of a0 ->
@@ -755,7 +755,7 @@ let object_define_own_prop runs0 s c l x desc throw =
                                              | Coq_attributes_accessor_of aa ->
                                                if attributes_change_accessor_on_non_configurable_dec
                                                     aa desc0
-                                               then reject s1 throw0
+                                               then reject s1 throwcont0
                                                else object_define_own_prop_write
                                                       s1 a)
                                        else (fun s message ->
@@ -764,10 +764,10 @@ let object_define_own_prop runs0 s c l x desc throw =
   Coq_result_impossible)
                                               s0
                                               ("cases are mutually exclusives in [defineOwnProperty]")))))
-      (fun default ->
+      (fun def ->
       if_some (run_object_method object_define_own_prop_ s l) (fun b ->
         match b with
-        | Coq_builtin_define_own_prop_default -> default s x desc throw
+        | Coq_builtin_define_own_prop_default -> def s x desc throwcont
         | Coq_builtin_define_own_prop_array ->
           if_spec
             (runs0.runs_type_object_get_own_prop s c l
@@ -810,13 +810,13 @@ let object_define_own_prop runs0 s c l x desc throw =
                                             (fun newLenDesc ->
                                             if le_int_decidable oldLen0
                                                  newLen
-                                            then default s2
+                                            then def s2
                                                    ("length")
-                                                   newLenDesc throw
+                                                   newLenDesc throwcont
                                             else if not_decidable
                                                       (bool_decidable
                                                         a.attributes_data_writable)
-                                                 then reject s2 throw
+                                                 then reject s2 throwcont
                                                  else let_binding
                                                         (match newLenDesc.descriptor_writable with
                                                          | Some b0 ->
@@ -835,10 +835,10 @@ let object_define_own_prop runs0 s c l x desc throw =
                                                            else newLenDesc)
                                                           (fun newLenDesc0 ->
                                                           if_bool
-                                                            (default s2
+                                                            (def s2
                                                               ("length")
                                                               newLenDesc0
-                                                              throw)
+                                                              throwcont)
                                                             (fun s3 succ ->
                                                             if not_decidable
                                                                  (bool_decidable
@@ -854,12 +854,12 @@ let object_define_own_prop runs0 s c l x desc throw =
                                                                    oldLen0
                                                                    newLenDesc0
                                                                    newWritable
-                                                                   throw
-                                                                   default))))))
+                                                                   throwcont
+                                                                   def))))))
                                | None ->
-                                 default s0
+                                 def s0
                                    ("length")
-                                   desc throw)
+                                   desc throwcont)
                          else if_spec
                                 (to_uint32 runs0 s0 c (Coq_value_prim
                                   (Coq_prim_string x))) (fun s1 ilen ->
@@ -912,13 +912,13 @@ let object_define_own_prop runs0 s c l x desc throw =
                                               (not_decidable
                                                 (bool_decidable
                                                   a.attributes_data_writable))
-                                         then reject s3 throw
+                                         then reject s3 throwcont
                                          else if_bool
-                                                (default s3 x desc false)
+                                                (def s3 x desc false)
                                                 (fun s4 b0 ->
                                                 if not_decidable
                                                      (bool_decidable b0)
-                                                then reject s4 throw
+                                                then reject s4 throwcont
                                                 else if le_int_decidable
                                                           oldLen0 index
                                                      then let a0 =
@@ -931,7 +931,7 @@ let object_define_own_prop runs0 s c l x desc throw =
                                                               (of_int
                                                                 (index +. 1.)))))
                                                           in
-                                                          default s4
+                                                          def s4
                                                             ("length")
                                                             a0 false
                                                      else res_ter s4
@@ -939,7 +939,7 @@ let object_define_own_prop runs0 s c l x desc throw =
                                                               (Coq_value_prim
                                                               (Coq_prim_bool
                                                               true)))))
-                                  else default s2 x desc throw))))
+                                  else def s2 x desc throwcont))))
                    | Coq_value_object l0 ->
                      (fun s message ->
   print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
@@ -959,7 +959,7 @@ let object_define_own_prop runs0 s c l x desc throw =
             if_some lmapo (fun lmap ->
               if_spec (runs0.runs_type_object_get_own_prop s c lmap x)
                 (fun s0 d ->
-                if_bool (default s0 x desc false) (fun s1 b0 ->
+                if_bool (def s0 x desc false) (fun s1 b0 ->
                   if b0
                   then let_binding (fun s2 ->
                          res_ter s2
@@ -984,9 +984,9 @@ let object_define_own_prop runs0 s c l x desc throw =
                                   | Some v ->
                                     if_void
                                       (runs0.runs_type_object_put s1 c lmap x
-                                        v throw) (fun s2 -> follow0 s2)
+                                        v throwcont) (fun s2 -> follow0 s2)
                                   | None -> follow0 s1))
-                  else reject s1 throw)))))))
+                  else reject s1 throwcont)))))))
 
 (** val run_to_descriptor :
     runs_type -> state -> execution_ctx -> value -> descriptor specres **)
@@ -2535,18 +2535,18 @@ let run_construct runs0 s c co l args =
 let run_call_default runs0 s c lf =
   let_binding
     (result_out (Coq_out_ter (s, (res_val (Coq_value_prim Coq_prim_undef)))))
-    (fun default ->
+    (fun def ->
     if_some (run_object_method object_code_ s lf) (fun oC ->
       match oC with
       | Some bd ->
         if list_eq_nil_decidable (prog_elements (funcbody_prog bd))
-        then default
+        then def
         else if_success_or_return
                (runs0.runs_type_prog s c (funcbody_prog bd)) (fun s' ->
                result_out (Coq_out_ter (s',
                  (res_val (Coq_value_prim Coq_prim_undef))))) (fun s' rv ->
                result_out (Coq_out_ter (s', (res_normal rv))))
-      | None -> default))
+      | None -> def))
 
 (** val creating_function_object_proto :
     runs_type -> state -> execution_ctx -> object_loc -> result **)
@@ -3035,11 +3035,11 @@ let run_object_get_own_prop runs0 s c l x =
           (if_some_or_default
             (convert_option_attributes
               (Heap.read_option string_comparable p x))
-            Coq_full_descriptor_undef id))) (fun default ->
+            Coq_full_descriptor_undef id))) (fun def ->
       match b with
-      | Coq_builtin_get_own_prop_default -> default s
+      | Coq_builtin_get_own_prop_default -> def s
       | Coq_builtin_get_own_prop_args_obj ->
-        if_spec (default s) (fun s1 d ->
+        if_spec (def s) (fun s1 d ->
           match d with
           | Coq_full_descriptor_undef ->
             res_spec s1 Coq_full_descriptor_undef
@@ -3068,7 +3068,7 @@ let run_object_get_own_prop runs0 s c l x =
                             s3
                             ("[run_object_get_own_prop]:  received an accessor property descriptor in a point where the specification suppose it never happens.")))))))
       | Coq_builtin_get_own_prop_string ->
-        if_spec (default s) (fun s0 d ->
+        if_spec (def s) (fun s0 d ->
           match d with
           | Coq_full_descriptor_undef ->
             if_spec
@@ -4523,7 +4523,7 @@ let run_expr_function runs0 s c fo args bd =
 
 let entering_eval_code runs0 s c direct bd k =
   let_binding
-    (coq_or (funcbody_is_strict bd) ((&&) direct c.execution_ctx_strict))
+    (coq_or (funcbody_is_strict bd) ( direct && c.execution_ctx_strict))
     (fun str ->
     let_binding (if direct then c else execution_ctx_initial str) (fun c' ->
       let_binding
@@ -4879,8 +4879,8 @@ let run_stat_try runs0 s c t1 t2o t3o =
     match t3o with
     | Some t3 ->
       if_success (runs0.runs_type_stat s1 c t3) (fun s2 rv' -> res_ter s2 r)
-    | None -> res_ter s1 r) (fun finally ->
-    if_any_or_throw (runs0.runs_type_stat s c t1) finally (fun s1 v ->
+    | None -> res_ter s1 r) (fun finallycont ->
+    if_any_or_throw (runs0.runs_type_stat s c t1) finallycont (fun s1 v ->
       match t2o with
       | Some y ->
         let (x, t2) = y in
@@ -4900,8 +4900,8 @@ let run_stat_try runs0 s c t1 t2o t3o =
                  (env_record_create_set_mutable_binding runs0 s' c l x None v
                    throw_irrelevant) (fun s2 ->
                  let c' = execution_ctx_with_lex c lex' in
-                 if_ter (runs0.runs_type_stat s2 c' t2) finally))))
-      | None -> finally s1 (res_throw (Coq_resvalue_value v))))
+                 if_ter (runs0.runs_type_stat s2 c' t2) finallycont))))
+      | None -> finallycont s1 (res_throw (Coq_resvalue_value v))))
 
 (** val run_stat_throw :
     runs_type -> state -> execution_ctx -> expr -> result **)
@@ -5587,14 +5587,14 @@ let run_call_prealloc runs0 s c b vthis args =
   Coq_result_impossible)
                   s
                   ("Value is callable, but isn\'t an object.")
-              | Coq_value_object this ->
+              | Coq_value_object thisobj ->
                 (match argArray with
                  | Coq_value_prim p ->
                    (match p with
                     | Coq_prim_undef ->
-                      runs0.runs_type_call s c this thisArg []
+                      runs0.runs_type_call s c thisobj thisArg []
                     | Coq_prim_null ->
-                      runs0.runs_type_call s c this thisArg []
+                      runs0.runs_type_call s c thisobj thisArg []
                     | Coq_prim_bool b0 -> run_error s Coq_native_error_type
                     | Coq_prim_number n -> run_error s Coq_native_error_type
                     | Coq_prim_string s0 -> run_error s Coq_native_error_type)
@@ -5607,7 +5607,7 @@ let run_call_prealloc runs0 s c b vthis args =
                        if_spec
                          (run_get_args_for_apply runs0 s1 c array 0. ilen)
                          (fun s2 arguments ->
-                         runs0.runs_type_call s2 c this thisArg arguments)))))
+                         runs0.runs_type_call s2 c thisobj thisArg arguments)))))
         else run_error s Coq_native_error_type))
   | Coq_prealloc_function_proto_call ->
     if is_callable_dec s vthis
@@ -5619,9 +5619,9 @@ let run_call_prealloc runs0 s c b vthis args =
   Coq_result_impossible)
               s
               ("Value is callable, but isn\'t an object.")
-          | Coq_value_object this ->
+          | Coq_value_object thisobj ->
             let (thisArg, a) = get_arg_first_and_rest args in
-            runs0.runs_type_call s c this thisArg a)
+            runs0.runs_type_call s c thisobj thisArg a)
     else run_error s Coq_native_error_type
   | Coq_prealloc_function_proto_bind ->
     if is_callable_dec s vthis
@@ -5633,7 +5633,7 @@ let run_call_prealloc runs0 s c b vthis args =
   Coq_result_impossible)
               s
               ("Value is callable, but isn\'t an object.")
-          | Coq_value_object this ->
+          | Coq_value_object thisobj ->
             let (vthisArg, a) = get_arg_first_and_rest args in
             let_binding
               (object_new (Coq_value_object (Coq_object_loc_prealloc
@@ -5642,7 +5642,7 @@ let run_call_prealloc runs0 s c b vthis args =
               let_binding (object_with_get o1 Coq_builtin_get_function)
                 (fun o2 ->
                 let_binding
-                  (object_with_details o2 None None None (Some this) (Some
+                  (object_with_details o2 None None None (Some thisobj) (Some
                     vthisArg) (Some a) None) (fun o3 ->
                   let_binding
                     (object_set_class o3
@@ -5662,12 +5662,12 @@ let run_call_prealloc runs0 s c b vthis args =
                           let (l, s') = object_alloc s o7 in
                           let_binding
                             (if_some
-                              (run_object_method object_class_ s' this)
+                              (run_object_method object_class_ s' thisobj)
                               (fun class0 ->
                               if string_comparable class0
                                    ("Function")
                               then if_number
-                                     (run_object_get runs0 s' c this
+                                     (run_object_get runs0 s' c thisobj
                                        ("length"))
                                      (fun s'0 n ->
                                      if_spec
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index 8dc8963bab0e14f66821d053a058b26171241ff1..2b1b250de65876f0191042dc838cad7c0af84863 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -85,7 +85,7 @@ let to_string = (fun f ->
 
 (** val neg : number -> number **)
 
-let neg = (~-.)
+let neg = (float_neg)
 
 (** val floor : number -> number **)
 
@@ -99,29 +99,32 @@ let absolute = abs_float
 
 let sign = (fun f -> float_of_int (float_compare f 0.))
 
-(** val lt_bool : number -> number -> bool **)
+(*
+   (** val lt_bool : number -> number -> bool **)
 
-let lt_bool = (<)
+   let lt_bool = (<)
 
-(** val add : number -> number -> number **)
+   (** val add : number -> number -> number **)
 
-let add = (+.)
+   let add = (+.)
 
-(** val sub : number -> number -> number **)
+   (** val sub : number -> number -> number **)
 
-let sub = (-.)
+   let sub = (-.)
 
-(** val fmod : number -> number -> number **)
+   (** val fmod : number -> number -> number **)
 
-let fmod = mod_float
+   let fmod = mod_float
 
-(** val mult : number -> number -> number **)
+   (** val mult : number -> number -> number **)
 
-let mult = ( *. )
+   let mult = ( *. )
 
-(** val div : number -> number -> number **)
+   (** val div : number -> number -> number **)
 
-let div = (/.)
+   let div = (/.)
+
+*)
 
 (** val number_comparable : number coq_Comparable **)
 
@@ -147,8 +150,8 @@ let classify_float n =
 let to_int32 = fun n ->
   match classify_float n with
   | FP_normal -> (* ARTHUR hacked this from | FP_normal | FP_subnormal *)
-    let i32 = 2. ** 32. in
-    let i31 = 2. ** 31. in
+    let i32 = float_exp 2. 32. in
+    let i31 = float_exp 2. 31. in
     let posint = (if n < 0. then (-1.) else 1.) *. (floor (abs_float n)) in
     let int32bit =
       let smod = mod_float posint i32 in
@@ -162,7 +165,7 @@ let to_int32 = fun n ->
 let to_uint32 = fun n ->
   match classify_float n with
   | FP_normal -> (* ARTHUR hacked this from | FP_normal | FP_subnormal *)
-    let i32 = 2. ** 32. in
+    let i32 = float_exp 2. 32. in
     let posint = (if n < 0. then (-1.) else 1.) *. (floor (abs_float n)) in
     let int32bit =
       let smod = mod_float posint i32 in
@@ -202,8 +205,8 @@ let int32_right_shift = (fun x y -> Int32.to_float (Int32.shift_right (Int32.of_
 (** val uint32_right_shift : float -> float -> float **)
 
 let uint32_right_shift = (fun x y ->
-  let i31 = 2. ** 31. in
-  let i32 = 2. ** 32. in
+  let i31 = float_exp 2. 31. in
+  let i32 = float_exp 2. 32. in
   let newx = if x >= i31 then x -. i32 else x in
   let r = Int32.to_float (Int32.shift_right_logical (Int32.of_float newx) (int_of_float y)) in
   if r < 0. then r +. i32 else r)
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index ac9e48e6e892bccc63e51e75b37b4c9b5e7b856c..41c64f5ba6fd21fd7ff4b14d51f585c7b1c79b14 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -109,7 +109,7 @@ and stat =
 | Coq_stat_switch  [@f labels, arg, body] of label_set * expr * switchbody (** Auto Generated Attributes **)
 and switchbody =
 | Coq_switchbody_nodefault  [@f clauses] of switchclause list (** Auto Generated Attributes **)
-| Coq_switchbody_withdefault  [@f clauses_before, default, clauses_after] of switchclause list * stat list * switchclause list (** Auto Generated Attributes **)
+| Coq_switchbody_withdefault  [@f clauses_before, clause_default, clauses_after] of switchclause list * stat list * switchclause list (** Auto Generated Attributes **)
 and switchclause =
 | Coq_switchclause_intro  [@f arg, stats] of expr * stat list (** Auto Generated Attributes **)
 and prog =
diff --git a/generator/tests/jsref/JsSyntaxAux.ml b/generator/tests/jsref/JsSyntaxAux.ml
index 079c0da83d69bfffef0fda0e4f6ddbc91e8d6465..4b5e221cc0a045e6b971d08db4d941fae173cc79 100644
--- a/generator/tests/jsref/JsSyntaxAux.ml
+++ b/generator/tests/jsref/JsSyntaxAux.ml
@@ -336,7 +336,7 @@ let object_for_array o defineownproperty =
     coq_object -> object_loc -> builtin_get -> builtin_get_own_prop ->
     builtin_define_own_prop -> builtin_delete -> coq_object **)
 
-let object_for_args_object o paramsmap get getownproperty defineownproperty delete =
+let object_for_args_object o paramsmap get getownproperty defineownproperty delete_prop =
   let { object_proto_ = x1; object_class_ = x2; object_extensible_ = x3;
     object_prim_value_ = x4; object_properties_ = x5; object_get_ = x6;
     object_get_own_prop_ = x7; object_get_prop_ = x8; object_put_ = x9;
@@ -350,7 +350,7 @@ let object_for_args_object o paramsmap get getownproperty defineownproperty dele
   { object_proto_ = x1; object_class_ = x2; object_extensible_ = x3;
   object_prim_value_ = x4; object_properties_ = x5; object_get_ = get;
   object_get_own_prop_ = getownproperty; object_get_prop_ = x8; object_put_ =
-  x9; object_can_put_ = x10; object_has_prop_ = x11; object_delete_ = delete;
+  x9; object_can_put_ = x10; object_has_prop_ = x11; object_delete_ = delete_prop;
   object_default_value_ = x13; object_define_own_prop_ = defineownproperty;
   object_construct_ = x15; object_call_ = x16; object_has_instance_ = x17;
   object_scope_ = x18; object_formal_parameters_ = x19; object_code_ = x20;
diff --git a/generator/tests/jsref/JsSyntaxInfos.ml b/generator/tests/jsref/JsSyntaxInfos.ml
index 7ef6cd1bbfc34ef306715a9b60da17e6fe093208..b6c9031c06c3a62820d1254d942c6f602be54201 100644
--- a/generator/tests/jsref/JsSyntaxInfos.ml
+++ b/generator/tests/jsref/JsSyntaxInfos.ml
@@ -58,7 +58,7 @@ and add_infos_stat str labs t =
    | Coq_stat_block ts -> Coq_stat_block (map f ts)
    | Coq_stat_var_decl vars ->
      Coq_stat_var_decl
-       (map (fun var -> let (s, eo) = var in (s, (opt fe eo))) vars)
+       (map (fun x -> let (s, eo) = x in (s, (opt fe eo))) vars)
    | Coq_stat_if (e, t0, to0) -> Coq_stat_if ((fe e), (f t0), (opt f to0))
    | Coq_stat_do_while (l, t0, e) ->
      Coq_stat_do_while ((label_set_add_empty labs), (f t0), (fe e))
@@ -69,15 +69,15 @@ and add_infos_stat str labs t =
    | Coq_stat_return eo -> Coq_stat_return (opt fe eo)
    | Coq_stat_break lopt -> Coq_stat_break lopt
    | Coq_stat_continue lopt -> Coq_stat_continue lopt
-   | Coq_stat_try (t0, catch, to0) ->
+   | Coq_stat_try (t0, catch_stat, to0) ->
      Coq_stat_try ((f t0),
-       (opt (fun c -> let (cs, t1) = c in (cs, (f t1))) catch), (opt f to0))
+       (opt (fun c -> let (cs, t1) = c in (cs, (f t1))) catch_stat), (opt f to0))
    | Coq_stat_for (l, eo1, eo2, eo3, t0) ->
      Coq_stat_for ((label_set_add_empty labs), (opt fe eo1), (opt fe eo2),
        (opt fe eo3), (f t0))
    | Coq_stat_for_var (l, vars, eo2, eo3, t0) ->
      Coq_stat_for_var ((label_set_add_empty labs),
-       (map (fun var -> let (s, eo) = var in (s, (opt fe eo))) vars), (opt fe eo2),
+       (map (fun x -> let (s, eo) = x in (s, (opt fe eo))) vars), (opt fe eo2),
        (opt fe eo3), (f t0))
    | Coq_stat_for_in (l, e1, e2, t0) ->
      Coq_stat_for_in ((label_set_add_empty labs), (fe e1), (fe e2), (f t0))
diff --git a/generator/tests/jsref/LibList.ml b/generator/tests/jsref/LibList.ml
index c72c1770dc4452f75877c6375be9038cc38e7eef..c10c0286f03f08e549d3e3efe4f185dff522ac46 100644
--- a/generator/tests/jsref/LibList.ml
+++ b/generator/tests/jsref/LibList.ml
@@ -1,6 +1,5 @@
 open LibOperation
 open LibReflect
-open Peano
 
 (** val list_eq_nil_decidable : 'a1 list -> coq_Decidable **)
 
@@ -48,7 +47,7 @@ let rev l =
 (** val length : 'a1 list -> int **)
 
 let length l =
-  fold_right (fun x acc -> plus 1 acc) 0 l
+  fold_right (fun x acc -> 1 + acc) 0 l
 
 (** val take_drop_last : 'a1 list -> 'a1 list * 'a1 **)
 
diff --git a/generator/tests/jsref/List0.ml b/generator/tests/jsref/List0.ml
index 909d21b8614bccbf59828e6e4beb1f29754a8ab3..74481c3f395992e28956c080a8ef4d22b222c3cb 100644
--- a/generator/tests/jsref/List0.ml
+++ b/generator/tests/jsref/List0.ml
@@ -1,7 +1,7 @@
 (** val hd : 'a1 -> 'a1 list -> 'a1 **)
 
-let hd default l = match l with
-| [] -> default
+let hd d l = match l with
+| [] -> d
 | x :: l0 -> x
 
 (** val tl : 'a1 list -> 'a1 list **)
diff --git a/generator/tests/jsref/Peano.ml b/generator/tests/jsref/Peano.ml
deleted file mode 100644
index d3bd560b116e119312927ed5711549ec71ac166f..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/Peano.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-(** val plus : int -> int -> int **)
-
-let rec plus = (+)
-
-(** val nat_iter : int -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
-
-let rec nat_iter n f x =
-  if int_eq n 0 then x else f (nat_iter (n-1) f x)
-
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index f811d694b29789a731f51a983931d3378412531b..164ce319557754461beef0d80c828bc4838d2ac1 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -16,10 +16,6 @@ let option_case d f o = match o with
 
 let int_of_char = (fun c -> float_of_int (int_of_char c))
 
-(** val ascii_comparable : char coq_Comparable **)
-
-let ascii_comparable = (=)
-
 (** val string_sub : string -> int -> int -> string **)
 
 let string_sub s n l =
@@ -27,15 +23,15 @@ let string_sub s n l =
 
 (** val lt_int_decidable : float -> float -> coq_Decidable **)
 
-let lt_int_decidable = (<)
+let lt_int_decidable x y = float_lt x y
 
 (** val le_int_decidable : float -> float -> coq_Decidable **)
 
-let le_int_decidable = (<=)
+let le_int_decidable x y = float_le x y
 
 (** val ge_nat_decidable : int -> int -> coq_Decidable **)
 
-let ge_nat_decidable = int_ge
+let ge_nat_decidable x y = int_ge x y
 
 type 'a coq_Pickable_option =
   'a option
diff --git a/navig-driver.js b/navig-driver.js
index 45766212980651e94949335b351a1af9fc1cf0f9..7fb224c2f0038f4e5a652f4b1049946c76944e62 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -530,3 +530,4 @@ var parsedTree;
   }
 }));
 
+