diff --git a/generator/tests/jsref/JsInterpreterSrc.ml b/deprecated/JsInterpreterSrc.ml
similarity index 100%
rename from generator/tests/jsref/JsInterpreterSrc.ml
rename to deprecated/JsInterpreterSrc.ml
diff --git a/generator/TODO b/generator/TODO
index d03fb727451661cd67888d1a9651129cd7f67639..3aa1db872ebef05ec33a3adcd37d4c40c7388220 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -1,5 +1,67 @@
+(** val object_write : state -> object_loc -> coq_object -> state **)
+=> on pourrait faire
+(** val object_write : state -> object_loc -> coq_object -> unit*state **)
 
 
+ -----------
+
+    let_binding (fun s0 ->
+      if_value (def s0 l) (fun s_2 v ->
+        if spec_function_get_error_case_dec s_2 x v
+        then run_error s_2 Coq_native_error_type
+        else res_ter s_2 (res_val v))) (fun function0 -> ...)
+  
+ -----------
+   spec_function_get_error_case_dec (@pure)
+
+	let function0 = fun () -> (* implicity bind s0 *)
+		 let%value v = (def l) in     (* implicitly from s0 to s_2 *)
+		 let%ter_ro b = spec_function_get_error_case_dec x v in	 (* implicy pass s_2 en read-only *)
+       if b
+         then run_error Coq_native_error_type  (* on s2 implicitly *)
+         else return_val v)) (* res on s2 implicitly *) (* where  return_val v = res_ter (res_val v) *)
+   in ...
+
+
+ -----------
+
+state as last arg
+
+ -----------
+TODO inliner:
+	let if_any_or_throw w k1 k2 =
+	let if_success_or_return w k1 k2 =
+
+ -----------
+TODO 
+
+	let if_success_state rv w k =
+	=> inliner if_ter 
+	  et nommer la fonction à l'intérieur, qui est stateless
+
+ -----------
+
+inline or_decidable
+ and all of libreflect
+
+
+ ----
+ rename decl_env_record_pickable_option into
+ decl_env_record_option
+----------
+
+remove Coq_value_prim
+----
+
+(* TODO: one day
+    let%spec v1 = run_expr_get_value e1 in
+    let%spec v2 = run_expr_get_value e2 in
+    run_binary_op op v1 v2
+*)
+
+
+=========================================================
+
 list.rev on ctx
 
 display quotes 1717
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index ee4c829bcffd9858a0e2aea660faa97d4e392512..eec41271c28b75a9c421829fd3f12c581966571a 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -211,6 +211,9 @@ let ppf_record llde =
     | (lbl, exp) :: xs -> aux (acc ^ Printf.sprintf "%s: %s,@," lbl exp) xs
   in aux "" llde
 
+let ppf_record_with seinit slbl sexp =
+   ppf_apply "record_with" (show_list ",@ " [ seinit; Printf.sprintf "\"%s\"" slbl; sexp ])
+
 let ppf_decl id expr = Printf.sprintf "@[<v 0>%s: %s,@,@]" id expr
 
 let ppf_pat_array id_list array_expr =
@@ -788,9 +791,14 @@ 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,_)          -> 
+  | Texp_record     (llde,None)          -> 
       let sexp = ppf_record (List.map (fun (_, lbl, exp) -> (lbl.lbl_name, inline_of_wrap exp)) llde) in
       apply_dest' ctx dest sexp
+  | Texp_record  ([(_,lbl, exp)], Some einit) -> (* record_with(einit, lbl, exp) *)
+      let sexp = ppf_record_with (inline_of_wrap einit) (lbl.lbl_name) (inline_of_wrap exp) in
+      apply_dest' ctx dest sexp
+
+  | Texp_record (_,Some e0)  -> out_of_scope loc "record with multiple fields assigned"
   | Texp_field      (exp, _, lbl)     ->
       let sexp = ppf_field_access (inline_of_wrap exp) lbl.lbl_name in
       apply_dest' ctx dest sexp
diff --git a/generator/main.ml b/generator/main.ml
index d60b1a79cf1f67f450380bb4c2f8136d236e0209..1d5b5b9d2fa6d2c18fc18d03f344002149111ae8 100644
--- a/generator/main.ml
+++ b/generator/main.ml
@@ -34,15 +34,13 @@ let _ =
                       "includes a directory where to look for interface files");
        ("-o", Arg.String (fun s -> outputfile := Some s), "set the output file name");
        ("-debug", Arg.Set debug, "trace the various steps");
+       ("-dsource", Arg.Set Clflags.dump_source, "dump source after ppx");
        ("-ppx", Arg.String (add_to_list Clflags.all_ppx (* TODO Compenv.first_ppx *) ), "load ppx");
        ("-mode", Arg.String (fun s -> set_current_mode s), "current mode: unlog, log, or token")
      ]
      (fun f -> files := f :: !files)
      ("usage: [-I dir] [..other options..] file.ml");
 
-   (* force: -dsource *)
-   Clflags.dump_source := true;
-
 
    files := List.rev !files;
    if List.length !files <> 1 then
diff --git a/generator/monad_ppx.ml b/generator/monad_ppx.ml
index 4795795ea1995145d6a310aa4f6584c3fcbf0423..0edbe2737bc0e04000a8ba097374bdbc480390d3 100644
--- a/generator/monad_ppx.ml
+++ b/generator/monad_ppx.ml
@@ -5,7 +5,9 @@ open Parsetree
 open Longident
 
 let monad_mapping =
-   [("spec", "if_spec");
+   [("run", "if_run");
+    (*("spec", "if_spec");  *)
+    ("string", "if_string");
     (*("success", "ifsuccess")*)
    ]
 
@@ -26,6 +28,7 @@ becomes
 let generate_mapper namesid = function argv ->
   { default_mapper with
     expr = fun mapper expr ->
+      let aux e = mapper.expr mapper e in
       match expr with
       (* Is this an extension node? *)
       | { pexp_desc =
@@ -48,8 +51,8 @@ let generate_mapper namesid = function argv ->
             Exp.apply ~loc (Exp.ident
                               (Location.mkloc
                                  (Longident.Lident ident) Location.none))
-              [("", e);
-               ("", Exp.fun_ "" None p1 (Exp.fun_ "" None p2 cont))]
+              [("", aux e);
+               ("", Exp.fun_ "" None p1 (Exp.fun_ "" None p2 (aux cont)))]
           | _ ->
             raise (Location.Error (
                 Location.error ~loc ("error with let%"^name)))
diff --git a/generator/parse_type.ml b/generator/parse_type.ml
index 96beaf616d8a0f95a4fe5ad73ca9656beb46ad14..f423a9a51e9375f6f513a9cbc81c8c6d095532c3 100644
--- a/generator/parse_type.ml
+++ b/generator/parse_type.ml
@@ -107,7 +107,7 @@ let process_implementation_file ppf sourcefile =
   try
     let env = initial_env () in
     let parsetree = parse_file inputfile Parse.implementation ast_impl_magic_number in
-
+    if !Clflags.dump_source then fprintf ppf "%a@." Pprintast.structure parsetree;
 
     let typedtree = Typemod.type_implementation sourcefile prefixname modulename env parsetree in
     (Some (parsetree, typedtree), inputfile, modulename)
diff --git a/generator/stdlib_ml/stdlib.js b/generator/stdlib_ml/stdlib.js
index 62d1f9a2c227270e95e19874f9789de77f278f12..95ded7b43f72f9fa43398412af04742ee2a474e4 100644
--- a/generator/stdlib_ml/stdlib.js
+++ b/generator/stdlib_ml/stdlib.js
@@ -1,3 +1,11 @@
+function record_with(einit, lbl, exp) {
+  var res = {};
+  for (var i in einit) {
+    res[i] = einit[i];
+  }
+  res[lbl] = exp;
+  return res;
+}
 
 //----------------------------------------------------------------------------
 
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index 15a8e718b651e0ef821e6233319747ef4e35a1d2..ea2b460ad362437aafdce0a2e571225bddf7a2f4 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -116,6 +116,7 @@ val float_le : float -> float -> bool*)
 val bool_eq : bool -> bool -> bool (* should be "===" in  JS *)
 val ( && ) : bool -> bool -> bool  (* beware of strict vs lazy semantics: todo discuss --> just map to  *)
 val not : bool -> bool
+val ( || ) : bool -> bool -> bool  (* beware of strict vs lazy semantics: todo discuss --> just map to  *)
 
 
 (*--------------------*)
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index da300106cb3833eba62ba9fb7f5e3ffbde609609..f7a7ff69791801095376cf0f14270ee169ec6fad 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -159,39 +159,37 @@ let attributes_enumerable _foo_ = match _foo_ with
 (** val state_with_object_heap :
     state -> (object_loc, coq_object) Heap.heap -> state **)
 
+(* STATEFUL *)
 let state_with_object_heap s new_object_heap =
-  let { state_object_heap = old_object_heap; state_env_record_heap =
-    env_heap; state_fresh_locations = fresh_locs; state_event_list =
-    ev_list } = s
-  in
-  { state_object_heap = new_object_heap; state_env_record_heap = env_heap;
-  state_fresh_locations = fresh_locs; state_event_list = ev_list }
+  { s with state_object_heap = new_object_heap } 
 
 (** val state_map_object_heap :
     state -> ((object_loc, coq_object) Heap.heap -> (object_loc, coq_object)
     Heap.heap) -> state **)
 
+(* STATEFUL *)
 let state_map_object_heap s f =
   state_with_object_heap s (f s.state_object_heap)
 
 (** val object_write : state -> object_loc -> coq_object -> state **)
 
+(* STATEFUL *)
 let object_write s l o =
   state_map_object_heap s (fun h -> Heap.write h l o)
 
 (** val object_alloc : state -> coq_object -> object_loc * state **)
 
+(* STATEFUL *)
 let object_alloc s o =
   let { state_object_heap = cells; state_env_record_heap = bindings;
-    state_fresh_locations = state_fresh_locations0; state_event_list =
-    ev_list } = s
+    state_fresh_locations = state_fresh_locations0; } = s
   in
   let n = state_fresh_locations0 in
   let alloc = state_fresh_locations0 + 1 in
   let l = Coq_object_loc_normal n in
   (l,
   (object_write { state_object_heap = cells; state_env_record_heap =
-    bindings; state_fresh_locations = alloc; state_event_list = ev_list } l
+    bindings; state_fresh_locations = alloc } l
     o))
 
 (** val object_map_properties :
@@ -284,38 +282,40 @@ let mutability_of_bool _foo_ = match _foo_ with
 (** val state_with_env_record_heap :
     state -> (env_loc, env_record) Heap.heap -> state **)
 
+(* STATEFUL *)
 let state_with_env_record_heap s new_env_heap =
   let { state_object_heap = object_heap; state_env_record_heap =
-    old_env_heap; state_fresh_locations = fresh_locs; state_event_list =
-    ev_list } = s
+    old_env_heap; state_fresh_locations = fresh_locs; } = s
   in
   { state_object_heap = object_heap; state_env_record_heap = new_env_heap;
-  state_fresh_locations = fresh_locs; state_event_list = ev_list }
+  state_fresh_locations = fresh_locs }
 
 (** val state_map_env_record_heap :
     state -> ((env_loc, env_record) Heap.heap -> (env_loc, env_record)
     Heap.heap) -> state **)
 
+(* STATEFUL *)
 let state_map_env_record_heap s f =
   state_with_env_record_heap s (f s.state_env_record_heap)
 
 (** val env_record_write : state -> env_loc -> env_record -> state **)
 
+(* STATEFUL *)
 let env_record_write s l e =
   state_map_env_record_heap s (fun h -> Heap.write h l e)
 
 (** val env_record_alloc : state -> env_record -> int * state **)
 
+(* STATEFUL *)
 let env_record_alloc s e =
   let { state_object_heap = cells; state_env_record_heap = bindings;
-    state_fresh_locations = state_fresh_locations0; state_event_list =
-    ev_list } = s
+    state_fresh_locations = state_fresh_locations0;  } = s
   in
   let l =  state_fresh_locations0 in
   let alloc = state_fresh_locations0 + 1 in
   let bindings' = Heap.write bindings l e in
   (l, { state_object_heap = cells; state_env_record_heap = bindings';
-  state_fresh_locations = alloc; state_event_list = ev_list })
+  state_fresh_locations = alloc })
 
 (** val provide_this_true : provide_this_flag **)
 
@@ -352,6 +352,7 @@ let decl_env_record_rem ed x =
 (** val env_record_write_decl_env :
     state -> env_loc -> prop_name -> mutability -> value -> state **)
 
+(* STATEFUL *)
 let env_record_write_decl_env s l x mu v =
   match Heap.read nat_eq s.state_env_record_heap l with
   | Coq_env_record_decl ed ->
@@ -362,17 +363,20 @@ let env_record_write_decl_env s l x mu v =
 (** val lexical_env_alloc :
     state -> int list -> env_record -> int list * state **)
 
+(* STATEFUL *)
 let lexical_env_alloc s lex e =
   let (l, s') = env_record_alloc s e in let lex' = l :: lex in (lex', s')
 
 (** val lexical_env_alloc_decl : state -> int list -> int list * state **)
 
+(* STATEFUL *)
 let lexical_env_alloc_decl s lex =
   lexical_env_alloc s lex (Coq_env_record_decl decl_env_record_empty)
 
 (** val lexical_env_alloc_object :
     state -> int list -> object_loc -> provide_this_flag -> int list * state **)
 
+(* STATEFUL *)
 let lexical_env_alloc_object s lex l pt =
   lexical_env_alloc s lex (Coq_env_record_object (l, pt))
 
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index e987f11c51359813be647fdae35989da5408ae86..3004b16ad72f3546af3e04c6164dd5de1892debf 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -199,12 +199,14 @@ let ref_kind_comparable x y =
 (** val object_binds_pickable_option :
     state -> object_loc -> coq_object coq_Pickable_option **)
 
+(* STATEFUL-RO *)
 let object_binds_pickable_option s l =
   Heap.read_option object_loc_comparable s.state_object_heap l
 
 (** val env_record_binds_pickable_option :
     state -> env_loc -> env_record coq_Pickable_option **)
 
+(* STATEFUL-RO *)
 let env_record_binds_pickable_option s l =
   Heap.read_option nat_eq s.state_env_record_heap l
 
@@ -261,6 +263,7 @@ let attributes_is_data_dec a = match a with
     state -> object_loc -> (object_properties_type -> object_properties_type)
     -> state option **)
 
+(* STATEFUL -- idea is to have this one imperative *)
 let run_object_heap_map_properties s l f =
   map (fun o -> object_write s l (object_map_properties o f))
     (object_binds_pickable_option s l)
@@ -269,6 +272,7 @@ let run_object_heap_map_properties s l f =
     state -> object_loc -> (object_properties_type -> object_properties_type)
     -> state coq_Pickable_option **)
 
+(* STATEFUL -- eliminate by inlining *)
 let object_heap_map_properties_pickable_option s l f =
   run_object_heap_map_properties s l f
 
@@ -373,10 +377,12 @@ let attributes_change_accessor_on_non_configurable_dec aa desc =
 
 (** val run_function_get_error_case : state -> prop_name -> value -> bool **)
 
+(* STATEFUL-RO *)
 let run_function_get_error_case s x v =
 match v with
 | Coq_value_prim w -> false
 | Coq_value_object l ->
+    (* In strict mode, cannot call "caller" *)
     (if string_comparable x ("caller")
      then true
      else false)
@@ -388,11 +394,13 @@ match v with
 (** val spec_function_get_error_case_dec :
     state -> prop_name -> value -> coq_Decidable **)
 
+(* STATEFUL-RO *)
 let spec_function_get_error_case_dec s x v =
   run_function_get_error_case s x v
 
 (** val run_callable : state -> value -> call option option **)
 
+(* STATEFUL-RO *)
 let run_callable s v = 
 match v with
 | Coq_value_prim w -> Some None
@@ -402,12 +410,14 @@ match v with
 
 (** val is_callable_dec : state -> value -> coq_Decidable **)
 
+(* STATEFUL-RO *)
 let is_callable_dec s v =
   option_case false (fun o -> option_case false (fun x -> true) o) (run_callable s v)
 
 (** val object_properties_keys_as_list_pickable_option :
     state -> object_loc -> prop_name list coq_Pickable_option **)
 
+(* STATEFUL-RO *)
 let object_properties_keys_as_list_pickable_option s l =
   map (fun props -> LibList.map fst (Heap.to_list string_comparable props))
     (map object_properties_ (object_binds_pickable_option s l))
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index d65bd24311f315085b0665c7c19f798c88b61108..58a86ebe703b07dd3c13e6a78c41c419c9810958 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -1343,7 +1343,8 @@ let dummy_fresh_locations = 0
 (** val state_initial : state **)
 
 let state_initial =
-  { state_object_heap = object_heap_initial; state_env_record_heap =
-    env_record_heap_initial; state_fresh_locations = dummy_fresh_locations;
-    state_event_list = [] }
+  { state_object_heap = object_heap_initial; 
+    state_env_record_heap = env_record_heap_initial; 
+    state_fresh_locations = dummy_fresh_locations;
+     }
 
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 15fa2f819328976f1f2268967b01be02f33e66a7..b76b6f32baa39ab978ea4c03dcc265fc2adbdb2a 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -3170,6 +3170,7 @@ and run_block s c _foo_ = match _foo_ with
     state -> execution_ctx -> binary_op -> expr -> expr ->
     result **)
 
+(* TODO: DEPRECATED 
 and run_expr_binary_op s c op e1 e2 =
   match is_lazy_op op with
   | Some b_ret ->
@@ -3184,9 +3185,26 @@ and run_expr_binary_op s c op e1 e2 =
       if_spec (run_expr_get_value s1 c e2) (fun s2 v2 ->
         run_binary_op s2 c op v1 v2))
 
+*)
+
+and run_expr_binary_op s c op e1 e2 =
+  match is_lazy_op op with
+  | Some b_ret ->
+    if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
+      let_binding (convert_value_to_boolean v1) (fun b1 ->
+        if bool_comparable b1 b_ret
+        then res_ter s1 (res_val v1)
+        else if_spec (run_expr_get_value s1 c e2) (fun s2 v ->
+               res_ter s2 (res_val v))))
+  | None ->
+    let%run (s1,v1) = run_expr_get_value s c e1 in
+    let%run (s2,v2) = run_expr_get_value s1 c e2 in
+    run_binary_op s2 c op v1 v2
+
 (** val run_expr_access :
     state -> execution_ctx -> expr -> expr -> result **)
 
+(* TODO DEPRECATEd
 and run_expr_access s c e1 e2 =
   if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
     if_spec (run_expr_get_value s1 c e2) (fun s2 v2 ->
@@ -3196,6 +3214,16 @@ and run_expr_access s c e1 e2 =
       else if_string (to_string s2 c v2) (fun s3 x ->
              res_ter s3
                (res_ref (ref_create_value v1 x c.execution_ctx_strict)))))
+*)
+
+and run_expr_access s c e1 e2 =
+  let%run (s1,v1) = run_expr_get_value s c e1 in
+  let%run (s2,v2) = run_expr_get_value s1 c e2 in
+   if    (value_comparable v1 (Coq_value_prim Coq_prim_undef))
+      || (value_comparable v1 (Coq_value_prim Coq_prim_null))
+   then run_error s2 Coq_native_error_type
+   else let%string (s3,x) = to_string s2 c v2 in
+        res_ter s3 (res_ref (ref_create_value v1 x c.execution_ctx_strict))
 
 (** val run_expr_assign :
     state -> execution_ctx -> binary_op option -> expr -> expr
@@ -3542,7 +3570,7 @@ and run_stat_switch s c labs e sb =
   if_spec (run_expr_get_value s c e) (fun s1 vi ->
     let_binding (fun w ->
       if_success
-        (if_break w (fun s2 r ->
+        (if_break (w) (fun s2 r ->
           if res_label_in r labs
           then result_out (Coq_out_ter (s2, (res_normal r.res_value)))
           else result_out (Coq_out_ter (s2, r)))) (fun s0 r ->
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index 1c87e563b0f0db1df006eda25a5d19a313fec7ee..794dc667fdfb310c5ebd0ff9609dda9e6d73c95b 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -137,10 +137,9 @@ let if_success_state rv w k =
           (if resvalue_comparable r.res_value Coq_resvalue_empty
            then rv
            else r.res_value))
-    | Coq_restype_break -> res_ter s0 (res_overwrite_value_if_empty rv r)
-    | Coq_restype_continue -> res_ter s0 (res_overwrite_value_if_empty rv r)
-    | Coq_restype_return -> res_ter s0 (res_overwrite_value_if_empty rv r)
-    | Coq_restype_throw -> res_ter s0 r)
+    | Coq_restype_throw -> res_ter s0 r
+    | _ -> res_ter s0 (res_overwrite_value_if_empty rv r)
+    )
 
 (** val if_success :
     result -> (state -> resvalue -> 'a1 specres) -> 'a1 specres **)
@@ -193,12 +192,8 @@ let if_any_or_throw w k1 k2 =
     | Coq_restype_return -> k1 s r
     | Coq_restype_throw ->
       (match r.res_value with
-       | Coq_resvalue_empty ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_any_or_throw] called with a non-value result.")
        | Coq_resvalue_value v -> if_empty_label s r (fun x -> k2 s v)
-       | Coq_resvalue_ref r0 ->
+       | _ ->
          (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
            ("[if_any_or_throw] called with a non-value result.")))
@@ -291,23 +286,12 @@ let if_string w k =
     match v with
     | Coq_value_prim p ->
       (match p with
-       | Coq_prim_undef ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_string] called on a non-string value.")
-       | Coq_prim_null ->
+       | Coq_prim_string s0 -> k s s0
+       | _ ->
          (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
-           ("[if_string] called on a non-string value.")
-       | Coq_prim_bool b ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_string] called on a non-string value.")
-       | Coq_prim_number n ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_string] called on a non-string value.")
-       | Coq_prim_string s0 -> k s s0)
+           ("[if_string] called on a non-string value.")       
+       )
     | Coq_value_object o ->
       (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
@@ -321,23 +305,12 @@ let if_number w k =
     match v with
     | Coq_value_prim p ->
       (match p with
-       | Coq_prim_undef ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_number] called with non-number value.")
-       | Coq_prim_null ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_number] called with non-number value.")
-       | Coq_prim_bool b ->
-         (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
-           s
-           ("[if_number] called with non-number value.")
        | Coq_prim_number n -> k s n
-       | Coq_prim_string s0 ->
+       | _ ->
          (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
            s
-           ("[if_number] called with non-number value."))
+           ("[if_number] called with non-number value.")
+       )
     | Coq_value_object o ->
       (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
@@ -382,6 +355,7 @@ let if_spec w k =
     | Coq_specret_out o -> if_abort o (fun x -> res_out o))
 
 
+let if_run w k = if_spec w k
 
 
 let ifx_prim w k = if_prim w k
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index eceb83836d96a37d48e9a9a12a52c2b188d35bc1..88138b812b1e8f322d2fe8bd6516fae7572497d4 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -571,8 +571,7 @@ type event =
 
 type state = { state_object_heap : (object_loc, coq_object) Heap.heap;
                state_env_record_heap : (env_loc, env_record) Heap.heap;
-               state_fresh_locations : int;
-               state_event_list : event list }
+               state_fresh_locations : int }
 
 (** val state_object_heap : state -> (object_loc, coq_object) Heap.heap **)
 
diff --git a/generator/tests/jsref/LibReflect.ml b/generator/tests/jsref/LibReflect.ml
index f71de61ab4ad96346a5023a426a03c0a7d9bb002..aecb210464c043bfd6c410ecc673aa0b260d0456 100644
--- a/generator/tests/jsref/LibReflect.ml
+++ b/generator/tests/jsref/LibReflect.ml
@@ -23,7 +23,7 @@ let bool_decidable b =
 (** val not_decidable : coq_Decidable -> coq_Decidable **)
 
 let not_decidable h =
-  neg h
+  not h
 
 (** val or_decidable : coq_Decidable -> coq_Decidable -> coq_Decidable **)
 
@@ -47,7 +47,7 @@ let comparable_of_dec h x y =
 (** val bool_comparable : bool coq_Comparable **)
 
 let bool_comparable x y =
-  eqb x y
+  bool_eq x y
 
 (** val prop_eq_decidable :
     coq_Decidable -> coq_Decidable -> coq_Decidable **)