diff --git a/coq/JsCommon.v b/coq/JsCommon.v
index ce358a55..4fa5ba96 100644
--- a/coq/JsCommon.v
+++ b/coq/JsCommon.v
@@ -871,13 +871,9 @@ Definition decl_env_record_rem Ed x : decl_env_record :=
 
 (** LATER: Change the following definition to a relation. *)
 
-Definition env_record_write_decl_env S L x mu v :=
-  match Heap.read (state_env_record_heap S) L with
-  | env_record_decl Ed =>
-     let env' := decl_env_record_write Ed x mu v in
-     env_record_write S L (env_record_decl env')
-  | env_record_object _ _ => S (* It should never happen *)
-  end.
+Definition env_record_write_decl_env S L Ed x mu v :=
+  env_record_write S L (env_record_decl 
+    (decl_env_record_write Ed x mu v)).
 
 
 (**************************************************************)
@@ -1219,7 +1215,6 @@ Inductive value_viewable_as : string -> state -> value -> prim -> Prop :=
 Definition is_syntactic_eval e :=
   match e with
   | expr_identifier s => decide (s = "eval")
-  | expr_literal (literal_string s) => decide (s = "eval")
   | _ => false
   end.
 
diff --git a/coq/JsCorrectness.v b/coq/JsCorrectness.v
index fbb79850..fca42c65 100644
--- a/coq/JsCorrectness.v
+++ b/coq/JsCorrectness.v
@@ -2800,10 +2800,10 @@ Proof.
 Qed.
 
 
-Lemma binding_inst_function_decls_correct : forall runs S C args L fds str bconfig o,
+Lemma binding_inst_function_decls_correct : forall runs S C L fds str bconfig o,
   runs_type_correct runs ->
   binding_inst_function_decls runs S C L fds str bconfig = o ->
-  red_expr S C (spec_binding_inst_function_decls args L fds str bconfig) o.
+  red_expr S C (spec_binding_inst_function_decls L fds str bconfig) o.
 Proof.
   introv IH HR. gen S o. induction fds; introv HR.
   simpls. run_inv. applys* red_spec_binding_inst_function_decls_nil.
@@ -2813,7 +2813,7 @@ Proof.
   let_name as M. rename a into fd. rename l into fo.
   asserts M_correct: (forall S o,
       M S = o ->
-      red_expr S C (spec_binding_inst_function_decls_5 args L fd fds str fo bconfig) o).
+      red_expr S C (spec_binding_inst_function_decls_5 L fd fds str fo bconfig) o).
     clears HR S o. introv HR. subst M.
     subst fname. run red_spec_binding_inst_function_decls_5
       using env_record_set_mutable_binding_correct.
@@ -2981,12 +2981,12 @@ Proof.
     clear EQA. apply~ red_spec_create_arguments_object_4.
 Qed.
 
-Lemma binding_inst_arg_obj_correct : forall runs S C lf p xs args L o,
+Lemma binding_inst_arg_obj_correct : forall runs S C lf str xs args L o,
   runs_type_correct runs ->
-  binding_inst_arg_obj runs S C lf p xs args L = o ->
-  red_expr S C (spec_binding_inst_arg_obj lf p xs args L) o.
+  binding_inst_arg_obj runs S C lf xs args L str = o ->
+  red_expr S C (spec_binding_inst_arg_obj lf xs args L str) o.
 Proof.
-  introv IH HR. unfolds in HR. let_name.
+  introv IH HR. unfolds in HR.
   run~ red_spec_binding_inst_arg_obj using create_arguments_object_correct.
   cases_if.
    run red_spec_binding_inst_arg_obj_1_strict
@@ -3165,9 +3165,11 @@ Proof.
       M vthis = o ->
       red_expr S0 C (expr_call_5 l is_eval_direct vs (out_ter S3 vthis)) o).
     clear HR S o. introv HR. subst M.
-    case_if.
-      subst. applys red_expr_call_5_eval. applys* run_eval_correct.
-      applys* red_expr_call_5_not_eval. apply* IH.
+    case_if as a.
+      destruct a as (a1&a2). apply bool_eq_true in a2. rewrite a2. subst_hyp a1.
+        applys red_expr_call_5_eval. applys* run_eval_correct.
+      applys* red_expr_call_5_not_eval. rew_logic in *. rew_reflect. eassumption.
+        apply* IH.
     clear EQM.
   subst. destruct rv; tryfalse.
     applys* red_expr_call_4_not_ref.
@@ -4991,7 +4993,8 @@ Proof.
   (* prealloc_global *)
   discriminate.
   (* prealloc_global_eval *)
-  discriminate.
+  apply red_spec_call_prealloc_global_eval.
+  applys* run_eval_correct.
   (* prealloc_global_parse_int *)
   discriminate.
   (* prealloc_global_parse_float *)
diff --git a/coq/JsInterpreter.v b/coq/JsInterpreter.v
index cc9f037e..265bf4fd 100644
--- a/coq/JsInterpreter.v
+++ b/coq/JsInterpreter.v
@@ -878,7 +878,7 @@ Definition env_record_set_mutable_binding runs S C L x v str : result_void :=
       if_some (Heap.read_option Ed x) (fun rm =>
         let '(mu, v_old) := rm in
         ifb mutability_is_mutable mu then
-          res_void (env_record_write_decl_env S L x mu v)
+          res_void (env_record_write_decl_env S L Ed x mu v)
         else out_error_or_void S str native_error_type)
     | env_record_object l pt =>
       object_put runs S C l x v str
@@ -934,7 +934,7 @@ Definition env_record_create_mutable_binding runs S C L x (deletable_opt : optio
       ifb decl_env_record_indom Ed x then
         impossible_with_heap_because S "Already declared environnment record in [env_record_create_mutable_binding]."
       else
-        'let S' := env_record_write_decl_env S L x (mutability_of_bool deletable) undef in
+        'let S' := env_record_write_decl_env S L Ed x (mutability_of_bool deletable) undef in
         res_void S'
     | env_record_object l pt =>
       if_bool (object_has_prop runs S C l x) (fun S1 has =>
@@ -957,7 +957,7 @@ Definition env_record_create_immutable_binding S L x : result_void :=
       ifb decl_env_record_indom Ed x then
         impossible_with_heap_because S "Already declared environnment record in [env_record_create_immutable_binding]."
       else
-        res_void (env_record_write_decl_env S L x mutability_uninitialized_immutable undef)
+        res_void (env_record_write_decl_env S L Ed x mutability_uninitialized_immutable undef)
     | env_record_object _ _ =>
         impossible_with_heap_because S "[env_record_create_immutable_binding] received an environnment record object."
     end).
@@ -968,7 +968,7 @@ Definition env_record_initialize_immutable_binding S L x v : result_void :=
     | env_record_decl Ed =>
       if_some (pick_option (Heap.binds Ed x)) (fun evs =>
         ifb evs = (mutability_uninitialized_immutable, undef) then
-          'let S' := env_record_write_decl_env S L x mutability_immutable v in
+          'let S' := env_record_write_decl_env S L Ed x mutability_immutable v in
           res_void S'
         else
           impossible_with_heap_because S "Non suitable binding in [env_record_initialize_immutable_binding].")
@@ -1356,16 +1356,15 @@ Definition create_arguments_object runs S C lf xs args X str : result :=
         if_bool (object_define_own_prop runs S2 C l "callee" A false) (fun S3 b' =>
           res_ter S3 l)))).
 
-Definition binding_inst_arg_obj runs S C lf p xs args L : result_void :=
+Definition binding_inst_arg_obj runs S C lf xs args L str : result_void :=
   let arguments := "arguments" in
-  'let str := prog_intro_strictness p in
-    if_object (create_arguments_object runs S C lf xs args
-                   (execution_ctx_variable_env C) str) (fun S1 largs =>
-      if str then
-        if_void (env_record_create_immutable_binding S1 L arguments) (fun S2 =>
-          env_record_initialize_immutable_binding S2 L arguments largs)
-      else
-        env_record_create_set_mutable_binding runs S1 C L arguments None largs false).
+  if_object (create_arguments_object runs S C lf xs args
+                 (execution_ctx_variable_env C) str) (fun S1 largs =>
+    if str then
+      if_void (env_record_create_immutable_binding S1 L arguments) (fun S2 =>
+        env_record_initialize_immutable_binding S2 L arguments largs)
+    else
+      env_record_create_set_mutable_binding runs S1 C L arguments None largs false).
 
 Fixpoint binding_inst_var_decls runs S C L (vds : list string) bconfig str : result_void :=
   match vds with
@@ -1396,7 +1395,7 @@ Definition execution_ctx_binding_inst runs S C (ct : codetype) (funco : option o
             in
           match ct, funco, bdefined with
           | codetype_func, Some func, false =>
-            if_void (binding_inst_arg_obj runs S2 C func p names args L) follow2
+            if_void (binding_inst_arg_obj runs S2 C func names args L str) follow2
           | codetype_func, _, false =>
             impossible_with_heap_because S2 "Weird `arguments' object in [execution_ctx_binding_inst]."
           | _, _, _ => follow2 S2
@@ -2083,8 +2082,8 @@ Definition run_expr_call runs S C e1 e2s : result :=
           *)
           ifb (is_callable S3 l) then
             'let follow := fun vthis =>
-              ifb l = prealloc_global_eval then
-                run_eval runs S3 C is_eval_direct vs
+              ifb l = prealloc_global_eval /\ is_eval_direct then
+                run_eval runs S3 C true vs
               else runs_type_call runs S3 C l vthis vs in
             match rv with
             | resvalue_value v => follow undef
@@ -2638,6 +2637,9 @@ Definition run_array_join_elements runs S C l (k length : int) (sep : string) sR
 Definition run_call_prealloc runs S C B vthis (args : list value) : result :=
   match B with
 
+  | prealloc_global_eval =>
+     run_eval runs S C false args
+
   | prealloc_global_is_nan =>
     'let v := get_arg 0 args in
     if_number (to_number runs S C v) (fun S0 n =>
diff --git a/coq/JsPrettyInterm.v b/coq/JsPrettyInterm.v
index 71d35969..f6f41c93 100644
--- a/coq/JsPrettyInterm.v
+++ b/coq/JsPrettyInterm.v
@@ -336,17 +336,17 @@ Inductive ext_expr :=
   | spec_binding_inst_formal_params_2 : list value -> env_loc -> string -> list string -> strictness_flag -> value -> out -> ext_expr
   | spec_binding_inst_formal_params_3 : list value -> env_loc -> string -> list string -> strictness_flag -> value -> ext_expr
   | spec_binding_inst_formal_params_4 : list value -> env_loc -> list string -> strictness_flag -> out -> ext_expr
-  | spec_binding_inst_function_decls :  list value -> env_loc -> list funcdecl -> strictness_flag -> bool -> ext_expr
-  | spec_binding_inst_function_decls_1 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_2 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_3 : list value -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> specret full_descriptor -> ext_expr
-  | spec_binding_inst_function_decls_3a : list value -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> full_descriptor -> ext_expr
-  | spec_binding_inst_function_decls_4 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_5 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> ext_expr
-  | spec_binding_inst_function_decls_6 : list value -> env_loc -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
-  | spec_binding_inst_arg_obj :   object_loc -> prog -> list string -> list value -> env_loc -> ext_expr
-  | spec_binding_inst_arg_obj_1 : prog -> env_loc -> strictness_flag -> out -> ext_expr
-  | spec_binding_inst_arg_obj_2 : prog -> env_loc -> object_loc -> out -> ext_expr
+  | spec_binding_inst_function_decls :  env_loc -> list funcdecl -> strictness_flag -> bool -> ext_expr
+  | spec_binding_inst_function_decls_1 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_2 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_3 : funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> specret full_descriptor -> ext_expr
+  | spec_binding_inst_function_decls_3a : funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> full_descriptor -> ext_expr
+  | spec_binding_inst_function_decls_4 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_5 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> ext_expr
+  | spec_binding_inst_function_decls_6 : env_loc -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
+  | spec_binding_inst_arg_obj :   object_loc -> list string -> list value -> env_loc -> strictness_flag -> ext_expr
+  | spec_binding_inst_arg_obj_1 : env_loc -> strictness_flag -> out -> ext_expr
+  | spec_binding_inst_arg_obj_2 : env_loc -> object_loc -> out -> ext_expr
   | spec_binding_inst_var_decls : env_loc -> list string -> bool -> strictness_flag -> ext_expr
   | spec_binding_inst_var_decls_1 : env_loc -> string -> list string -> bool -> strictness_flag -> out -> ext_expr
   | spec_binding_inst_var_decls_2 : env_loc -> list string -> bool -> strictness_flag -> out -> ext_expr
@@ -1148,17 +1148,17 @@ Definition out_of_ext_expr (e : ext_expr) : option out :=
   | spec_binding_inst_formal_params_2 _ _ _ _ _ _ o => Some o
   | spec_binding_inst_formal_params_3 _ _ _ _ _ _ => None
   | spec_binding_inst_formal_params_4 _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_1 _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_2 _ _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_3 _ _ _ _ _ _ y => out_of_specret y
-  | spec_binding_inst_function_decls_3a _ _ _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_4 _ _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_5 _ _ _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_6 _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls _ _ _ _ => None
+  | spec_binding_inst_function_decls_1 _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_2 _ _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_3 _ _ _ _ _ y => out_of_specret y
+  | spec_binding_inst_function_decls_3a _ _ _ _ _ _ => None
+  | spec_binding_inst_function_decls_4 _ _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_5 _ _ _ _ _ _ => None
+  | spec_binding_inst_function_decls_6 _ _ _ _ o => Some o
   | spec_binding_inst_arg_obj   object_loc _ _ _ _ => None
-  | spec_binding_inst_arg_obj_1 _ _ _ o => Some o
-  | spec_binding_inst_arg_obj_2 _ _ _ o => Some o
+  | spec_binding_inst_arg_obj_1 _ _ o => Some o
+  | spec_binding_inst_arg_obj_2 _ _ o => Some o
   | spec_binding_inst_var_decls _ _ _ _ => None
   | spec_binding_inst_var_decls_1 _ _ _ _ _ o => Some o
   | spec_binding_inst_var_decls_2 _ _ _ _ o => Some o
diff --git a/coq/JsPrettyRules.v b/coq/JsPrettyRules.v
index c1529bf1..c588fde7 100644
--- a/coq/JsPrettyRules.v
+++ b/coq/JsPrettyRules.v
@@ -1050,12 +1050,12 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
       red_expr S C (expr_call_5  l is_eval_direct vs (out_ter S undef)) o ->
       red_expr S C (expr_call_4 (resvalue_value v) l is_eval_direct vs) o
 
-  | red_expr_call_5_eval : forall S0 S C is_eval_direct vs v o, (* Step 8, special for eval *)
-      red_expr S C (spec_call_global_eval is_eval_direct vs) o ->
-      red_expr S0 C (expr_call_5 prealloc_global_eval is_eval_direct vs (out_ter S v)) o
+  | red_expr_call_5_eval : forall S0 S C vs v o, (* Step 8, special for eval *)
+      red_expr S C (spec_call_global_eval true vs) o ->
+      red_expr S0 C (expr_call_5 prealloc_global_eval true vs (out_ter S v)) o
 
    | red_expr_call_5_not_eval : forall S0 S C l is_eval_direct vs v o, (* Step 8 *)
-      l <> prealloc_global_eval ->
+      l <> prealloc_global_eval \/ !is_eval_direct ->
       red_expr S C (spec_call l v vs) o ->
       red_expr S0 C (expr_call_5 l is_eval_direct vs (out_ter S v)) o
 
@@ -2416,7 +2416,7 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
 
   | red_spec_env_record_create_mutable_binding_1_decl_indom : forall S C L x deletable Ed S',
       ~ decl_env_record_indom Ed x ->
-      S' = env_record_write_decl_env S L x (mutability_of_bool deletable) undef ->
+      S' = env_record_write_decl_env S L Ed x (mutability_of_bool deletable) undef ->
       red_expr S C (spec_env_record_create_mutable_binding_1 L x deletable (env_record_decl Ed)) (out_void S')
 
   | red_spec_env_record_create_mutable_binding_1_object : forall o1 S C L x deletable l pt o,
@@ -2443,7 +2443,7 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
   | red_spec_env_record_set_mutable_binding_1_decl_mutable : forall v_old mu S C L x v str Ed o,
       decl_env_record_binds Ed x mu v_old ->
       mutability_is_mutable mu ->
-      red_expr S C (spec_returns (out_void (env_record_write_decl_env S L x mu v))) o ->
+      red_expr S C (spec_returns (out_void (env_record_write_decl_env S L Ed x mu v))) o ->
       red_expr S C (spec_env_record_set_mutable_binding_1 L x v str (env_record_decl Ed)) o
 
   | red_spec_env_record_set_mutable_binding_1_decl_non_mutable : forall v_old mu S C L x v str Ed o,
@@ -2529,7 +2529,7 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
   | red_spec_env_record_create_immutable_binding : forall Ed S C L x S',
       env_record_binds S L (env_record_decl Ed) ->
       ~ decl_env_record_indom Ed x ->
-      S' = env_record_write_decl_env S L x mutability_uninitialized_immutable undef ->
+      S' = env_record_write_decl_env S L Ed x mutability_uninitialized_immutable undef ->
       red_expr S C (spec_env_record_create_immutable_binding L x) (out_void S')
 
   (** Initialize immutable binding (returns void) (10.2.1.1.8) *)
@@ -2537,7 +2537,7 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
   | red_spec_env_record_initialize_immutable_binding : forall Ed v_old S C L x v S',
       env_record_binds S L (env_record_decl Ed) ->
       decl_env_record_binds Ed x mutability_uninitialized_immutable v_old -> (* Note: v_old is always undef here *)
-      S' = env_record_write_decl_env S L x mutability_immutable v ->
+      S' = env_record_write_decl_env S L Ed x mutability_immutable v ->
       red_expr S C (spec_env_record_initialize_immutable_binding L x v) (out_void S')
 
   (** Auxiliary: combination of create mutable binding and set mutable binding (returns void) *)
@@ -2662,96 +2662,95 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
      bindings for function declarations (Step 5). *)
   (* LATER: remove "args" as it's not used at all in this subroutine *)
 
-  | red_spec_binding_inst_function_decls_nil : forall L S C args str bconfig, (* Step 5b *)
-      red_expr S C (spec_binding_inst_function_decls args L nil str bconfig) (out_void S)
+  | red_spec_binding_inst_function_decls_nil : forall L S C str bconfig, (* Step 5b *)
+      red_expr S C (spec_binding_inst_function_decls L nil str bconfig) (out_void S)
 
-  | red_spec_binding_inst_function_decls_cons : forall str_fd S C L args fd fds str bconfig o1 o, (* Step 5b *)
+  | red_spec_binding_inst_function_decls_cons : forall str_fd S C L fd fds str bconfig o1 o, (* Step 5b *)
       str_fd = funcbody_is_strict (funcdecl_body fd) ->
       red_expr S C (spec_creating_function_object (funcdecl_parameters fd) (funcdecl_body fd) (execution_ctx_variable_env C) str_fd) o1 ->
-      red_expr S C (spec_binding_inst_function_decls_1 args L fd fds str bconfig o1) o ->
-      red_expr S C (spec_binding_inst_function_decls args L (fd::fds) str bconfig) o
+      red_expr S C (spec_binding_inst_function_decls_1 L fd fds str bconfig o1) o ->
+      red_expr S C (spec_binding_inst_function_decls L (fd::fds) str bconfig) o
 
-  | red_spec_binding_inst_function_decls_1 : forall o1 L S0 S C args fd fds str fo bconfig o, (* Step 5c *)
+  | red_spec_binding_inst_function_decls_1 : forall o1 L S0 S C fd fds str fo bconfig o, (* Step 5c *)
       red_expr S C (spec_env_record_has_binding L (funcdecl_name fd)) o1 ->
-      red_expr S C (spec_binding_inst_function_decls_2 args L fd fds str fo bconfig o1) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_1 args L fd fds str bconfig (out_ter S fo)) o
+      red_expr S C (spec_binding_inst_function_decls_2 L fd fds str fo bconfig o1) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_1 L fd fds str bconfig (out_ter S fo)) o
 
-  | red_spec_binding_inst_function_decls_2_false : forall o1 L S0 S C args fd fds str fo bconfig o, (* Step 5d *)
+  | red_spec_binding_inst_function_decls_2_false : forall o1 L S0 S C fd fds str fo bconfig o, (* Step 5d *)
       red_expr S C (spec_env_record_create_mutable_binding L (funcdecl_name fd) (Some bconfig)) o1 ->
-      red_expr S C (spec_binding_inst_function_decls_4 args L fd fds str fo bconfig o1) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_2 args L fd fds str fo bconfig (out_ter S false)) o
+      red_expr S C (spec_binding_inst_function_decls_4 L fd fds str fo bconfig o1) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_2 L fd fds str fo bconfig (out_ter S false)) o
 
-  | red_spec_binding_inst_function_decls_2_true_global : forall S0 S C args fd fds str fo bconfig y1 o, (* Step 5e ii *)
+  | red_spec_binding_inst_function_decls_2_true_global : forall S0 S C fd fds str fo bconfig y1 o, (* Step 5e ii *)
       red_spec S C (spec_object_get_prop prealloc_global (funcdecl_name fd)) y1 ->
-      red_expr S C (spec_binding_inst_function_decls_3 args fd fds str fo bconfig y1) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_2 args env_loc_global_env_record fd fds str fo bconfig (out_ter S true)) o
+      red_expr S C (spec_binding_inst_function_decls_3 fd fds str fo bconfig y1) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_2 env_loc_global_env_record fd fds str fo bconfig (out_ter S true)) o
 
-  | red_spec_binding_inst_function_decls_3_true : forall S0 S C args fd fds str fo bconfig A Anew o1 o, (* Step 5e iii *)
+  | red_spec_binding_inst_function_decls_3_true : forall S0 S C fd fds str fo bconfig A Anew o1 o, (* Step 5e iii *)
       attributes_configurable A = true ->
       Anew = attributes_data_intro undef true true bconfig ->
       red_expr S C (spec_object_define_own_prop prealloc_global (funcdecl_name fd) Anew true) o1 ->
-      red_expr S C (spec_binding_inst_function_decls_4 args env_loc_global_env_record fd fds str fo bconfig o1) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_3 args fd fds str fo bconfig (ret S (full_descriptor_some A))) o
+      red_expr S C (spec_binding_inst_function_decls_4 env_loc_global_env_record fd fds str fo bconfig o1) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_3 fd fds str fo bconfig (ret S (full_descriptor_some A))) o
 
-  | red_spec_binding_inst_function_decls_4 : forall S0 S C args L fd fds str fo bconfig rv o, (* Step 5e iii *)
-      red_expr S C (spec_binding_inst_function_decls_5 args L fd fds str fo bconfig) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_4 args L fd fds str fo bconfig (out_ter S rv)) o
+  | red_spec_binding_inst_function_decls_4 : forall S0 S C L fd fds str fo bconfig rv o, (* Step 5e iii *)
+      red_expr S C (spec_binding_inst_function_decls_5 L fd fds str fo bconfig) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_4 L fd fds str fo bconfig (out_ter S rv)) o
 
-  | red_spec_binding_inst_function_decls_3_false : forall S0 S C args fd fds str fo A bconfig o, (* Step 5e iii, else *)
+  | red_spec_binding_inst_function_decls_3_false : forall S0 S C fd fds str fo A bconfig o, (* Step 5e iii, else *)
       attributes_configurable A = false ->
-      red_expr S C (spec_binding_inst_function_decls_3a args fd fds str fo bconfig A) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_3 args fd fds str fo bconfig (ret S (full_descriptor_some A))) o
+      red_expr S C (spec_binding_inst_function_decls_3a fd fds str fo bconfig A) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_3 fd fds str fo bconfig (ret S (full_descriptor_some A))) o
 
-  | red_spec_binding_inst_function_decls_3a_type_error : forall S C args fd fds str fo A bconfig o, (* Step 5e iv *)
+  | red_spec_binding_inst_function_decls_3a_type_error : forall S C fd fds str fo A bconfig o, (* Step 5e iv *)
       (* LATER: descriptor_is_accessor A \/ ~ (attributes_writable A = true /\ attributes_enumerable A = true) ->  *)
       descriptor_is_accessor A \/ attributes_writable A = false \/ attributes_enumerable A = false ->
       red_expr S C (spec_error native_error_type) o ->
-      red_expr S C (spec_binding_inst_function_decls_3a args fd fds str fo bconfig A) o
+      red_expr S C (spec_binding_inst_function_decls_3a fd fds str fo bconfig A) o
 
-  | red_spec_binding_inst_function_decls_3a_no_error : forall S C args fd fds str fo A bconfig o, (* Step 5e iv else *)
+  | red_spec_binding_inst_function_decls_3a_no_error : forall S C fd fds str fo A bconfig o, (* Step 5e iv else *)
       ~ (descriptor_is_accessor A \/ attributes_writable A = false \/ attributes_enumerable A = false) ->
-      red_expr S C (spec_binding_inst_function_decls_5 args env_loc_global_env_record fd fds str fo bconfig) o ->
-      red_expr S C (spec_binding_inst_function_decls_3a args fd fds str fo bconfig A) o
+      red_expr S C (spec_binding_inst_function_decls_5 env_loc_global_env_record fd fds str fo bconfig) o ->
+      red_expr S C (spec_binding_inst_function_decls_3a fd fds str fo bconfig A) o
 
-  | red_spec_binding_inst_function_decls_2_true : forall L S0 S C args fd fds str fo bconfig o, (* Step 5e *)
+  | red_spec_binding_inst_function_decls_2_true : forall L S0 S C fd fds str fo bconfig o, (* Step 5e *)
       L <> env_loc_global_env_record ->
-      red_expr S C (spec_binding_inst_function_decls_5 args L fd fds str fo bconfig) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_2 args L fd fds str fo bconfig (out_ter S true)) o
+      red_expr S C (spec_binding_inst_function_decls_5 L fd fds str fo bconfig) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_2 L fd fds str fo bconfig (out_ter S true)) o
 
-  | red_spec_binding_inst_function_decls_5 : forall o1 L S C args fd fds str fo bconfig o, (* Step 5f *)
+  | red_spec_binding_inst_function_decls_5 : forall o1 L S C fd fds str fo bconfig o, (* Step 5f *)
       red_expr S C (spec_env_record_set_mutable_binding L (funcdecl_name fd) (value_object fo) str) o1 ->
-      red_expr S C (spec_binding_inst_function_decls_6 args L fds str bconfig o1) o ->
-      red_expr S C (spec_binding_inst_function_decls_5 args L fd fds str fo bconfig) o
+      red_expr S C (spec_binding_inst_function_decls_6 L fds str bconfig o1) o ->
+      red_expr S C (spec_binding_inst_function_decls_5 L fd fds str fo bconfig) o
 
-  | red_spec_binding_inst_function_decls_6 : forall L S0 S C args fds str bconfig o, (* Step 5 loop *)
-      red_expr S C (spec_binding_inst_function_decls args L fds str bconfig) o ->
-      red_expr S0 C (spec_binding_inst_function_decls_6 args L fds str bconfig (out_void S)) o
+  | red_spec_binding_inst_function_decls_6 : forall L S0 S C fds str bconfig o, (* Step 5 loop *)
+      red_expr S C (spec_binding_inst_function_decls L fds str bconfig) o ->
+      red_expr S0 C (spec_binding_inst_function_decls_6 L fds str bconfig (out_void S)) o
 
   (* Auxiliary reductions for binding instantiation:
      Declaring Arguments Object (Step 7) *)
 
-  | red_spec_binding_inst_arg_obj : forall str o1 L S C lf code xs args o, (* Step 7a *)
-      str = prog_intro_strictness code ->
+  | red_spec_binding_inst_arg_obj : forall str o1 L S C lf xs args o, (* Step 7a *)
       (* We actually need the variable environment with its pointer to parent variable environment for arguments object since it creates function objects.
          But we forget the parents at the very first step of Declaration Binding Instantiation. We do not change execution context in Declaration Binding
          Instaniation. So it is save to take the variable environment from execution context here. For the right way to do, should it be saved at the first
          step and then propagated until this point? *)
       red_expr S C (spec_create_arguments_object lf xs args (execution_ctx_variable_env C) str) o1 ->
-      red_expr S C (spec_binding_inst_arg_obj_1 code L str o1) o ->
-      red_expr S C (spec_binding_inst_arg_obj lf code xs args L) o
+      red_expr S C (spec_binding_inst_arg_obj_1 L str o1) o ->
+      red_expr S C (spec_binding_inst_arg_obj lf xs args L str) o
 
-  | red_spec_binding_inst_arg_obj_1_strict : forall o1 L S0 S C code largs o, (* Step 7b i *)
+  | red_spec_binding_inst_arg_obj_1_strict : forall o1 L S0 S C largs o, (* Step 7b i *)
       red_expr S C (spec_env_record_create_immutable_binding L "arguments") o1 ->
-      red_expr S C (spec_binding_inst_arg_obj_2 code L largs o1) o ->
-      red_expr S0 C (spec_binding_inst_arg_obj_1 code L true (out_ter S largs)) o
+      red_expr S C (spec_binding_inst_arg_obj_2 L largs o1) o ->
+      red_expr S0 C (spec_binding_inst_arg_obj_1 L true (out_ter S largs)) o
 
-  | red_spec_binding_inst_arg_obj_2 : forall L S0 S C code largs o, (* Step 7b ii *)
+  | red_spec_binding_inst_arg_obj_2 : forall L S0 S C largs o, (* Step 7b ii *)
       red_expr S C (spec_env_record_initialize_immutable_binding L "arguments" (value_object largs)) o ->
-      red_expr S0 C (spec_binding_inst_arg_obj_2 code L largs (out_void S)) o
+      red_expr S0 C (spec_binding_inst_arg_obj_2 L largs (out_void S)) o
 
-  | red_spec_binding_inst_arg_obj_1_not_strict : forall L S0 S C code largs o, (* Step 7c *)
+  | red_spec_binding_inst_arg_obj_1_not_strict : forall L S0 S C largs o, (* Step 7c *)
       red_expr S C (spec_env_record_create_set_mutable_binding L "arguments" None largs false) o ->
-      red_expr S0 C (spec_binding_inst_arg_obj_1 code L false (out_ter S largs)) o
+      red_expr S0 C (spec_binding_inst_arg_obj_1 L false (out_ter S largs)) o
 
   (* Auxiliary reductions for binding instantiation:
      bindings for variable declarations (Step 8) *)
@@ -2802,7 +2801,7 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
   | red_spec_binding_inst_3 : forall bconfig L S C ct olf code fds xs args o1 o, (* Step 5 *)
       bconfig = (If ct = codetype_eval then true else false) -> (* Step 2 *)
       fds = prog_funcdecl code ->
-      red_expr S C (spec_binding_inst_function_decls args L fds (prog_intro_strictness code) bconfig) o1 ->
+      red_expr S C (spec_binding_inst_function_decls L fds (prog_intro_strictness code) bconfig) o1 ->
       red_expr S C (spec_binding_inst_4 ct olf code xs args bconfig L o1) o ->
       red_expr S C (spec_binding_inst_3 ct olf code xs args L) o
 
@@ -2816,7 +2815,7 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
       red_expr S C (spec_binding_inst_5 ct olf code xs args bconfig L) o
 
   | red_spec_binding_inst_6_arguments : forall o1 L S0 S C lf code xs args bconfig o, (* Step 7 *)
-      red_expr S C (spec_binding_inst_arg_obj lf code xs args L) o1 ->
+      red_expr S C (spec_binding_inst_arg_obj lf xs args L (prog_intro_strictness code)) o1 ->
       red_expr S C (spec_binding_inst_7 code bconfig L o1) o ->
       red_expr S0 C (spec_binding_inst_6 codetype_func (Some lf) code xs args bconfig L (out_ter S false)) o
 
@@ -3278,6 +3277,12 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
 (*------------------------------------------------------------*)
 (** ** Global object builtin functions (15.1) *)
 
+  (** Calling eval as a function *)
+
+  | red_spec_call_prealloc_global_eval : forall S C o vthis args,
+      red_expr S C (spec_call_global_eval false args) o ->
+      red_expr S C (spec_call_prealloc prealloc_global_eval vthis args) o
+
   (** Eval (returns value)  (15.1.2) *)
 
   | red_spec_call_global_eval : forall S C bdirect args v o,