From cc73052b15de438270f8de5f2d632a7578cf9da1 Mon Sep 17 00:00:00 2001
From: Jeremie Koenig <jeremie.koenig@yale.edu>
Date: Sun, 23 Sep 2018 01:28:11 -0400
Subject: [PATCH] Don't include the global environment in semantics

Global environments are used as intermediate constructions when defining
the step relation for individual languages, however there is no need to
include them in the common interface for small-step semantics.
---
 backend/Allocproof.v          |  10 +-
 backend/Asmgenproof0.v        |   2 +-
 backend/Cminor.v              |  16 +-
 backend/Debugvarproof.v       |   6 +-
 backend/Inliningproof.v       |   6 +-
 backend/Linearizeproof.v      |  10 +-
 backend/RTLgenproof.v         |  12 +-
 backend/Stackingproof.v       |  22 +--
 cfrontend/Clight.v            |   4 +-
 cfrontend/ClightBigstep.v     |  12 +-
 cfrontend/Cminorgenproof.v    |  14 +-
 cfrontend/Csem.v              |   2 +-
 cfrontend/Cshmgenproof.v      |   4 +-
 cfrontend/Cstrategy.v         |  72 ++++----
 cfrontend/Initializersproof.v |  14 +-
 cfrontend/SimplExprproof.v    |  24 +--
 cfrontend/SimplLocalsproof.v  |  18 +-
 common/Behaviors.v            |  29 ++--
 common/Determinism.v          |   4 +-
 common/Smallstep.v            | 311 +++++++++++++++++-----------------
 x86/Asmgenproof.v             |   8 +-
 21 files changed, 293 insertions(+), 307 deletions(-)

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 1804f46beb..7fddaf1472 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1847,8 +1847,8 @@ Lemma exec_moves:
   satisf rs ls e' ->
   wt_regset env rs ->
   exists ls',
-    star step tge (Block s f sp (expand_moves mv bb) ls m)
-               E0 (Block s f sp bb ls' m)
+    star (step tge) (Block s f sp (expand_moves mv bb) ls m)
+                 E0 (Block s f sp bb ls' m)
   /\ satisf rs ls' e.
 Proof.
 Opaque destroyed_by_op.
@@ -1908,8 +1908,8 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
            Val.has_type v (env res) ->
            agree_callee_save ls ls1 ->
            exists ls2,
-           star LTL.step tge (Block ts tf sp bb ls1 m)
-                          E0 (State ts tf sp pc ls2 m)
+           star (LTL.step tge) (Block ts tf sp bb ls1 m)
+                            E0 (State ts tf sp pc ls2 m)
            /\ satisf (rs#res <- v) ls2 e),
       match_stackframes
         (RTL.Stackframe res f sp pc rs :: s)
@@ -1990,7 +1990,7 @@ Qed.
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 ->
   forall S1', match_states S1 S1' ->
-  exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'.
+  exists S2', plus (LTL.step tge) S1' t S2' /\ match_states S2 S2'.
 Proof.
   induction 1; intros WT S1' MS; inv MS; try UseShape.
 
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 70c4323c5c..8b940428e7 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -860,7 +860,7 @@ Lemma exec_straight_steps_1:
   rs#PC = Vptr b ofs ->
   Genv.find_funct_ptr ge b = Some (Internal fn) ->
   code_tail (Ptrofs.unsigned ofs) (fn_code fn) c ->
-  plus step ge (State rs m) E0 (State rs' m').
+  plus (step ge) (State rs m) E0 (State rs' m').
 Proof.
   induction 1; intros.
   apply plus_one.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 11941da31a..4fab36b0cb 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -908,13 +908,13 @@ Lemma eval_funcall_exec_stmt_steps:
    eval_funcall ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step ge (Callstate fd args k m)
-              t (Returnstate res k m'))
+   star (step ge) (Callstate fd args k m)
+                t (Returnstate res k m'))
 /\(forall f sp e m s t e' m' out,
    exec_stmt ge f sp e m s t e' m' out ->
    forall k,
    exists S,
-   star step ge (State f s k sp e m) t S
+   star (step ge) (State f s k sp e m) t S
    /\ outcome_state_match sp e' m' f k out S).
 Proof.
   apply eval_funcall_exec_stmt_ind2; intros.
@@ -1070,8 +1070,8 @@ Lemma eval_funcall_steps:
    eval_funcall ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step ge (Callstate fd args k m)
-              t (Returnstate res k m').
+   star (step ge) (Callstate fd args k m)
+                t (Returnstate res k m').
 Proof (proj1 eval_funcall_exec_stmt_steps).
 
 Lemma exec_stmt_steps:
@@ -1079,19 +1079,19 @@ Lemma exec_stmt_steps:
    exec_stmt ge f sp e m s t e' m' out ->
    forall k,
    exists S,
-   star step ge (State f s k sp e m) t S
+   star (step ge) (State f s k sp e m) t S
    /\ outcome_state_match sp e' m' f k out S.
 Proof (proj2 eval_funcall_exec_stmt_steps).
 
 Lemma evalinf_funcall_forever:
   forall m fd args T k,
   evalinf_funcall ge m fd args T ->
-  forever_plus step ge (Callstate fd args k m) T.
+  forever_plus (step ge) (Callstate fd args k m) T.
 Proof.
   cofix CIH_FUN.
   assert (forall sp e m s T f k,
           execinf_stmt ge f sp e m s T ->
-          forever_plus step ge (State f s k sp e m) T).
+          forever_plus (step ge) (State f s k sp e m) T).
   cofix CIH_STMT.
   intros. inv H.
 
diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index d31c63ec74..c15fabb821 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -355,8 +355,8 @@ Qed.
 
 Lemma eval_add_delta_ranges:
   forall s f sp c rs m before after,
-  star step tge (State s f sp (add_delta_ranges before after c) rs m)
-             E0 (State s f sp c rs m).
+  star (step tge) (State s f sp (add_delta_ranges before after c) rs m)
+               E0 (State s f sp c rs m).
 Proof.
   intros. unfold add_delta_ranges.
   destruct (delta_state before after) as [killed born].
@@ -423,7 +423,7 @@ Qed.
 Theorem transf_step_correct:
   forall s1 t s2, step ge s1 t s2 ->
   forall ts1 (MS: match_states s1 ts1),
-  exists ts2, plus step tge ts1 t ts2 /\ match_states s2 ts2.
+  exists ts2, plus (step tge) ts1 t ts2 /\ match_states s2 ts2.
 Proof.
   induction 1; intros ts1 MS; inv MS; try (inv TRC).
 - (* getstack *)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 2dcb895687..4d8fc8df61 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -224,8 +224,8 @@ Lemma tr_moves_init_regs:
   (forall r, In r rdsts -> Ple r ctx2.(mreg)) ->
   list_forall2 (val_reg_charact F ctx1 rs1) vl rsrcs ->
   exists rs2,
-    star step tge (State stk f sp pc1 rs1 m)
-               E0 (State stk f sp pc2 rs2 m)
+    star (step tge) (State stk f sp pc1 rs1 m)
+                 E0 (State stk f sp pc2 rs2 m)
   /\ agree_regs F ctx2 (init_regs vl rdsts) rs2
   /\ forall r, Plt r ctx2.(dreg) -> rs2#r = rs1#r.
 Proof.
@@ -933,7 +933,7 @@ Theorem step_simulation:
   forall S1 t S2,
   step ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
-  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  (exists S2', plus (step tge) S1' t S2' /\ match_states S2 S2')
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
   induction 1; intros; inv MS.
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 10a3d8b2a4..8364e849f5 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -252,8 +252,8 @@ Lemma starts_with_correct:
   unique_labels c2 ->
   starts_with lbl c1 = true ->
   find_label lbl c2 = Some c3 ->
-  plus step tge (State s f sp c1 ls m)
-             E0 (State s f sp c3 ls m).
+  plus (step tge) (State s f sp c1 ls m)
+               E0 (State s f sp c3 ls m).
 Proof.
   induction c1.
   simpl; intros; discriminate.
@@ -456,8 +456,8 @@ Lemma add_branch_correct:
   transf_function f = OK tf ->
   is_tail k tf.(fn_code) ->
   find_label lbl tf.(fn_code) = Some c ->
-  plus step tge (State s tf sp (add_branch lbl k) ls m)
-             E0 (State s tf sp c ls m).
+  plus (step tge) (State s tf sp (add_branch lbl k) ls m)
+               E0 (State s tf sp c ls m).
 Proof.
   intros. unfold add_branch.
   caseEq (starts_with lbl k); intro SW.
@@ -556,7 +556,7 @@ Qed.
 Theorem transf_step_correct:
   forall s1 t s2, LTL.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
-  (exists s2', plus Linear.step tge s1' t s2' /\ match_states s2 s2')
+  (exists s2', plus (Linear.step tge) s1' t s2' /\ match_states s2 s2')
   \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
 Proof.
   induction 1; intros; try (inv MS).
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b003eb104c..3b2526201b 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -416,7 +416,7 @@ Lemma tr_move_correct:
   forall r1 ns r2 nd cs f sp rs m,
   tr_move f.(fn_code) ns r1 nd r2 ->
   exists rs',
-  star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
+  star (step tge) (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
   rs'#r2 = rs#r1 /\
   (forall r, r <> r2 -> rs'#r = rs#r).
 Proof.
@@ -474,7 +474,7 @@ Definition transl_expr_prop
     (ME: match_env map e le rs)
     (EXT: Mem.extends m tm),
   exists rs', exists tm',
-     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
+     star (step tge) (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
   /\ match_env map (set_optvar dst v e) le rs'
   /\ Val.lessdef v rs'#rd
   /\ (forall r, In r pr -> rs'#r = rs#r)
@@ -488,7 +488,7 @@ Definition transl_exprlist_prop
     (ME: match_env map e le rs)
     (EXT: Mem.extends m tm),
   exists rs', exists tm',
-     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
+     star (step tge) (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
   /\ match_env map e le rs'
   /\ Val.lessdef_list vl rs'##rl
   /\ (forall r, In r pr -> rs'#r = rs#r)
@@ -502,7 +502,7 @@ Definition transl_condexpr_prop
     (ME: match_env map e le rs)
     (EXT: Mem.extends m tm),
   exists rs', exists tm',
-     plus step tge (State cs f sp ns rs tm) E0 (State cs f sp (if v then ntrue else nfalse) rs' tm')
+     plus (step tge) (State cs f sp ns rs tm) E0 (State cs f sp (if v then ntrue else nfalse) rs' tm')
   /\ match_env map e le rs'
   /\ (forall r, In r pr -> rs'#r = rs#r)
   /\ Mem.extends m tm'.
@@ -947,7 +947,7 @@ Definition transl_exitexpr_prop
     (ME: match_env map e le rs)
     (EXT: Mem.extends m tm),
   exists nd, exists rs', exists tm',
-     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
+     star (step tge) (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
   /\ nth_error nexits x = Some nd
   /\ match_env map e le rs'
   /\ Mem.extends m tm'.
@@ -1298,7 +1298,7 @@ Theorem transl_step_correct:
   forall S1 t S2, CminorSel.step ge S1 t S2 ->
   forall R1, match_states S1 R1 ->
   exists R2,
-  (plus RTL.step tge R1 t R2 \/ (star RTL.step tge R1 t R2 /\ lt_state S2 S1))
+  (plus (RTL.step tge) R1 t R2 \/ (star (RTL.step tge) R1 t R2 /\ lt_state S2 S1))
   /\ match_states S2 R2.
 Proof.
   induction 1; intros R1 MSTATE; inv MSTATE.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index ffd9b2278d..e88543de58 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -909,7 +909,7 @@ Lemma save_callee_save_rec_correct:
   m |= range sp pos (size_callee_save_area_rec l pos) ** P ->
   agree_regs j ls rs ->
   exists rs', exists m',
-     star step tge
+     star (step tge)
         (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save_rec l pos k) rs m)
      E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
   /\ m' |= contains_callee_saves j sp pos l ls ** P
@@ -1000,9 +1000,9 @@ Lemma save_callee_save_correct:
   let ls1 := LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) in
   let rs1 := undef_regs destroyed_at_function_entry rs in
   exists rs', exists m',
-     star step tge
-        (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save fe k) rs1 m)
-     E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
+     star (step tge)
+          (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save fe k) rs1 m)
+       E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
   /\ m' |= contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0 ** P
   /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p)
   /\ agree_regs j ls1 rs'.
@@ -1050,9 +1050,9 @@ Lemma function_prologue_correct:
      Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp')
   /\ store_stack m2' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) parent = Some m3'
   /\ store_stack m3' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) ra = Some m4'
-  /\ star step tge
-         (State cs fb (Vptr sp' Ptrofs.zero) (save_callee_save fe k) rs1 m4')
-      E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs' m5')
+  /\ star (step tge)
+          (State cs fb (Vptr sp' Ptrofs.zero) (save_callee_save fe k) rs1 m4')
+       E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs' m5')
   /\ agree_regs j' ls1 rs'
   /\ agree_locs ls1 ls0
   /\ m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P
@@ -1171,7 +1171,7 @@ Lemma restore_callee_save_rec_correct:
   agree_unused ls0 rs ->
   (forall r, In r l -> mreg_within_bounds b r) ->
   exists rs',
-    star step tge
+    star (step tge)
       (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save_rec l ofs k) rs m)
    E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m)
   /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r))
@@ -1216,7 +1216,7 @@ Lemma restore_callee_save_correct:
   m |= frame_contents j sp ls ls0 pa ra ** P ->
   agree_unused j ls0 rs ->
   exists rs',
-    star step tge
+    star (step tge)
        (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save fe k) rs m)
     E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m)
   /\ (forall r,
@@ -1255,7 +1255,7 @@ Lemma function_epilogue_correct:
      load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) = Some pa
   /\ load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) = Some ra
   /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1'
-  /\ star step tge
+  /\ star (step tge)
        (State cs fb (Vptr sp' Ptrofs.zero) (restore_callee_save fe k) rs m')
     E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs1 m')
   /\ agree_regs j (return_regs ls0 ls) rs1
@@ -1804,7 +1804,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
 Theorem transf_step_correct:
   forall s1 t s2, Linear.step ge s1 t s2 ->
   forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'),
-  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
+  exists s2', plus (step tge) s1' t s2' /\ match_states s2 s2'.
 Proof.
   induction 1; intros;
   try inv MS;
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 7a4c49a2f3..160863aef5 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -715,11 +715,11 @@ Definition step2 (ge: genv) := step ge (function_entry2 ge).
 
 Definition semantics1 (p: program) :=
   let ge := globalenv p in
-  Semantics_gen step1 (initial_state p) final_state ge ge.
+  Semantics_gen (step1 ge) (initial_state p) final_state ge.
 
 Definition semantics2 (p: program) :=
   let ge := globalenv p in
-  Semantics_gen step2 (initial_state p) final_state ge ge.
+  Semantics_gen (step2 ge) (initial_state p) final_state ge.
 
 (** This semantics is receptive to changes in events. *)
 
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 92457586eb..48e5f98ac0 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -300,14 +300,14 @@ Lemma exec_stmt_eval_funcall_steps:
   (forall e le m s t le' m' out,
    exec_stmt ge e le m s t le' m' out ->
    forall f k, exists S,
-   star step1 ge (State f s k e le m) t S
+   star (step1 ge) (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S)
 /\
   (forall m fd args t m' res,
    eval_funcall ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step1 ge (Callstate fd args k m) t (Returnstate res k m')).
+   star (step1 ge) (Callstate fd args k m) t (Returnstate res k m')).
 Proof.
   apply exec_stmt_funcall_ind; intros.
 
@@ -478,7 +478,7 @@ Lemma exec_stmt_steps:
    forall e le m s t le' m' out,
    exec_stmt ge e le m s t le' m' out ->
    forall f k, exists S,
-   star step1 ge (State f s k e le m) t S
+   star (step1 ge) (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S.
 Proof (proj1 exec_stmt_eval_funcall_steps).
 
@@ -487,7 +487,7 @@ Lemma eval_funcall_steps:
    eval_funcall ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step1 ge (Callstate fd args k m) t (Returnstate res k m').
+   star (step1 ge) (Callstate fd args k m) t (Returnstate res k m').
 Proof (proj2 exec_stmt_eval_funcall_steps).
 
 Definition order (x y: unit) := False.
@@ -495,12 +495,12 @@ Definition order (x y: unit) := False.
 Lemma evalinf_funcall_forever:
   forall m fd args T k,
   evalinf_funcall ge m fd args T ->
-  forever_N step1 order ge tt (Callstate fd args k m) T.
+  forever_N (step1 ge) order tt (Callstate fd args k m) T.
 Proof.
   cofix CIH_FUN.
   assert (forall e le m s T f k,
           execinf_stmt ge e le m s T ->
-          forever_N step1 order ge tt (State f s k e le m) T).
+          forever_N (step1 ge) order tt (State f s k e le m) T).
   cofix CIH_STMT.
   intros. inv H.
 
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ffafc5d242..c42daf6c66 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1651,8 +1651,8 @@ Lemma match_is_call_cont:
   match_cont k tk cenv xenv cs ->
   Csharpminor.is_call_cont k ->
   exists tk',
-    star step tge (State tfn Sskip tk sp te tm)
-               E0 (State tfn Sskip tk' sp te tm)
+    star (step tge) (State tfn Sskip tk sp te tm)
+                 E0 (State tfn Sskip tk' sp te tm)
     /\ is_call_cont tk'
     /\ match_cont k tk' cenv nil cs.
 Proof.
@@ -1745,7 +1745,7 @@ Lemma switch_descent:
   exists k',
   transl_lblstmt_cont cenv xenv ls k k'
   /\ (forall f sp e m,
-      plus step tge (State f s k sp e m) E0 (State f body k' sp e m)).
+      plus (step tge) (State f s k sp e m) E0 (State f body k' sp e m)).
 Proof.
   induction ls; intros.
 - monadInv H. econstructor; split.
@@ -1765,8 +1765,8 @@ Lemma switch_ascent:
   forall k k1,
   transl_lblstmt_cont cenv xenv ls k k1 ->
   exists k2,
-  star step tge (State f (Sexit n) k1 sp e m)
-             E0 (State f (Sexit O) k2 sp e m)
+  star (step tge) (State f (Sexit n) k1 sp e m)
+               E0 (State f (Sexit O) k2 sp e m)
   /\ transl_lblstmt_cont cenv xenv ls' k k2.
 Proof.
   induction 1; intros.
@@ -1799,7 +1799,7 @@ Lemma switch_match_states:
     (MK: match_cont k tk cenv xenv cs)
     (TK: transl_lblstmt_cont cenv xenv ls tk tk'),
   exists S,
-  plus step tge (State tfn (Sexit O) tk' (Vptr sp Ptrofs.zero) te tm) E0 S
+  plus (step tge) (State tfn (Sexit O) tk' (Vptr sp Ptrofs.zero) te tm) E0 S
   /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e le m) S.
 Proof.
   intros. inv TK.
@@ -1946,7 +1946,7 @@ Definition measure (S: Csharpminor.state) : nat :=
 Lemma transl_step_correct:
   forall S1 t S2, Csharpminor.step ge S1 t S2 ->
   forall T1, match_states S1 T1 ->
-  (exists T2, plus step tge T1 t T2 /\ match_states S2 T2)
+  (exists T2, plus (step tge) T1 t T2 /\ match_states S2 T2)
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
 Proof.
   induction 1; intros T1 MSTATE; inv MSTATE.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 0c3e00de73..8d2d55acab 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -786,7 +786,7 @@ Inductive final_state: state -> int -> Prop :=
 (** Wrapping up these definitions in a small-step semantics. *)
 
 Definition semantics (p: program) :=
-  Semantics_gen step (initial_state p) final_state (globalenv p) (globalenv p).
+  Semantics_gen (step (globalenv p)) (initial_state p) final_state (globalenv p).
 
 (** This semantics has the single-event property. *)
 
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 09e31cb2b5..10bbee1a66 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1318,7 +1318,7 @@ Inductive match_transl: stmt -> cont -> stmt -> cont -> Prop :=
 Lemma match_transl_step:
   forall ts tk ts' tk' f te le m,
   match_transl (Sblock ts) tk ts' tk' ->
-  star step tge (State f ts' tk' te le m) E0 (State f ts (Kblock tk) te le m).
+  star (step tge) (State f ts' tk' te le m) E0 (State f ts (Kblock tk) te le m).
 Proof.
   intros. inv H.
   apply star_one. constructor.
@@ -1525,7 +1525,7 @@ Qed.
 Lemma transl_step:
   forall S1 t S2, Clight.step2 ge S1 t S2 ->
   forall T1, match_states S1 T1 ->
-  exists T2, plus step tge T1 t T2 /\ match_states S2 T2.
+  exists T2, plus (step tge) T1 t T2 /\ match_states S2 T2.
 Proof.
   induction 1; intros T1 MST; inv MST.
 
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 28c8eeb887..69fb4700c5 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -407,12 +407,12 @@ Hint Resolve context_compose contextlist_compose.
   if it cannot get stuck by doing silent transitions only. *)
 
 Definition safe (s: Csem.state) : Prop :=
-  forall s', star Csem.step ge s E0 s' ->
+  forall s', star (Csem.step ge) s E0 s' ->
   (exists r, final_state s' r) \/ (exists t, exists s'', Csem.step ge s' t s'').
 
 Lemma safe_steps:
   forall s s',
-  safe s -> star Csem.step ge s E0 s' -> safe s'.
+  safe s -> star (Csem.step ge) s E0 s' -> safe s'.
 Proof.
   intros; red; intros.
   eapply H. eapply star_trans; eauto.
@@ -420,16 +420,16 @@ Qed.
 
 Lemma star_safe:
   forall s1 s2 t s3,
-  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 t s3) ->
-  star Csem.step ge s1 t s3.
+  safe s1 -> star (Csem.step ge) s1 E0 s2 -> (safe s2 -> star (Csem.step ge) s2 t s3) ->
+  star (Csem.step ge) s1 t s3.
 Proof.
   intros. eapply star_trans; eauto. apply H1. eapply safe_steps; eauto. auto.
 Qed.
 
 Lemma plus_safe:
   forall s1 s2 t s3,
-  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 t s3) ->
-  plus Csem.step ge s1 t s3.
+  safe s1 -> star (Csem.step ge) s1 E0 s2 -> (safe s2 -> plus (Csem.step ge) s2 t s3) ->
+  plus (Csem.step ge) s1 t s3.
 Proof.
   intros. eapply star_plus_trans; eauto. apply H1. eapply safe_steps; eauto. auto.
 Qed.
@@ -706,12 +706,12 @@ Variable m: mem.
 Lemma eval_simple_steps:
    (forall a v, eval_simple_rvalue e m a v ->
     forall C, context RV RV C ->
-    star Csem.step ge (ExprState f (C a) k e m)
-                   E0 (ExprState f (C (Eval v (typeof a))) k e m))
+    star (Csem.step ge) (ExprState f (C a) k e m)
+                     E0 (ExprState f (C (Eval v (typeof a))) k e m))
 /\ (forall a b ofs, eval_simple_lvalue e m a b ofs ->
     forall C, context LV RV C ->
-    star Csem.step ge (ExprState f (C a) k e m)
-                   E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)).
+    star (Csem.step ge) (ExprState f (C a) k e m)
+                     E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)).
 Proof.
 
 Ltac Steps REC C' := eapply star_trans; [apply (REC C'); eauto | idtac | simpl; reflexivity].
@@ -754,15 +754,15 @@ Qed.
 Lemma eval_simple_rvalue_steps:
   forall a v, eval_simple_rvalue e m a v ->
   forall C, context RV RV C ->
-  star Csem.step ge (ExprState f (C a) k e m)
-                E0 (ExprState f (C (Eval v (typeof a))) k e m).
+  star (Csem.step ge) (ExprState f (C a) k e m)
+                   E0 (ExprState f (C (Eval v (typeof a))) k e m).
 Proof (proj1 eval_simple_steps).
 
 Lemma eval_simple_lvalue_steps:
   forall a b ofs, eval_simple_lvalue e m a b ofs ->
   forall C, context LV RV C ->
-  star Csem.step ge (ExprState f (C a) k e m)
-                E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m).
+  star (Csem.step ge) (ExprState f (C a) k e m)
+                   E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m).
 Proof (proj2 eval_simple_steps).
 
 Corollary eval_simple_rvalue_safe:
@@ -980,8 +980,8 @@ Hint Resolve contextlist'_head contextlist'_tail.
 Lemma eval_simple_list_steps:
   forall rl vl, eval_simple_list' rl vl ->
   forall C, contextlist' C ->
-  star Csem.step ge (ExprState f (C rl) k e m)
-                E0 (ExprState f (C (rval_list vl rl)) k e m).
+  star (Csem.step ge) (ExprState f (C rl) k e m)
+                   E0 (ExprState f (C (rval_list vl rl)) k e m).
 Proof.
   induction 1; intros.
 (* nil *)
@@ -1142,7 +1142,7 @@ End DECOMPOSITION.
 
 Lemma estep_simulation:
   forall S t S',
-  estep S t S' -> plus Csem.step ge S t S'.
+  estep S t S' -> plus (Csem.step ge) S t S'.
 Proof.
   intros. inv H.
 (* simple *)
@@ -1395,7 +1395,7 @@ Qed.
 
 Theorem step_simulation:
   forall S1 t S2,
-  step S1 t S2 -> plus Csem.step ge S1 t S2.
+  step S1 t S2 -> plus (Csem.step ge) S1 t S2.
 Proof.
   intros. inv H.
   apply estep_simulation; auto.
@@ -1434,7 +1434,7 @@ End STRATEGY.
 
 Definition semantics (p: program) :=
   let ge := globalenv p in
-  Semantics_gen step (initial_state p) final_state ge ge.
+  Semantics_gen (step ge) (initial_state p) final_state ge.
 
 (** This semantics is receptive to changes in events. *)
 
@@ -2183,34 +2183,34 @@ Lemma bigstep_to_steps:
   (forall e m a t m' v,
    eval_expression e m a t m' v ->
    forall f k,
-   star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m'))
+   star (step ge) (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m'))
 /\(forall e m K a t m' a',
    eval_expr e m K a t m' a' ->
    forall C f k, leftcontext K RV C ->
    simple a' = true /\ typeof a' = typeof a /\
-   star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m'))
+   star (step ge) (ExprState f (C a) k e m) t (ExprState f (C a') k e m'))
 /\(forall e m al t m' al',
    eval_exprlist e m al t m' al' ->
    forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 = true -> simplelist al2 = true ->
    simplelist al' = true /\
-   star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
-              t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m'))
+   star (step ge) (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
+                t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m'))
 /\(forall e m s t m' out,
    exec_stmt e m s t m' out ->
    forall f k,
    exists S,
-   star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S)
+   star (step ge) (State f s k e m) t S /\ outcome_state_match e m' f k out S)
 /\(forall m fd args t m' res,
    eval_funcall m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step ge (Callstate fd args k m) t (Returnstate res k m')).
+   star (step ge) (Callstate fd args k m) t (Returnstate res k m')).
 Proof.
   apply bigstep_induction; intros.
 (* expression, general *)
   exploit (H0 (fun x => x) f k). constructor. intros [A [B C]].
   assert (match a' with Eval _ _ => False | _ => True end ->
-          star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m')).
+          star (step ge) (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m')).
    intro. eapply star_right. eauto. left. eapply step_expr; eauto. traceEq.
   destruct a'; auto.
   simpl in B. rewrite B in C. inv H1. auto.
@@ -2617,7 +2617,7 @@ Lemma eval_expression_to_steps:
    forall e m a t m' v,
    eval_expression e m a t m' v ->
    forall f k,
-   star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m').
+   star (step ge) (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m').
 Proof (proj1 bigstep_to_steps).
 
 Lemma eval_expr_to_steps:
@@ -2625,7 +2625,7 @@ Lemma eval_expr_to_steps:
    eval_expr e m K a t m' a' ->
    forall C f k, leftcontext K RV C ->
    simple a' = true /\ typeof a' = typeof a /\
-   star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m').
+   star (step ge) (ExprState f (C a) k e m) t (ExprState f (C a') k e m').
 Proof (proj1 (proj2 bigstep_to_steps)).
 
 Lemma eval_exprlist_to_steps:
@@ -2633,8 +2633,8 @@ Lemma eval_exprlist_to_steps:
    eval_exprlist e m al t m' al' ->
    forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 = true -> simplelist al2 = true ->
    simplelist al' = true /\
-   star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
-              t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m').
+   star (step ge) (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
+                t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m').
 Proof (proj1 (proj2 (proj2 bigstep_to_steps))).
 
 Lemma exec_stmt_to_steps:
@@ -2642,7 +2642,7 @@ Lemma exec_stmt_to_steps:
    exec_stmt e m s t m' out ->
    forall f k,
    exists S,
-   star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S.
+   star (step ge) (State f s k e m) t S /\ outcome_state_match e m' f k out S.
 Proof (proj1 (proj2 (proj2 (proj2 bigstep_to_steps)))).
 
 Lemma eval_funcall_to_steps:
@@ -2650,7 +2650,7 @@ Lemma eval_funcall_to_steps:
   eval_funcall m fd args t m' res ->
   forall k,
   is_call_cont k ->
-  star step ge (Callstate fd args k m) t (Returnstate res k m').
+  star (step ge) (Callstate fd args k m) t (Returnstate res k m').
 Proof (proj2 (proj2 (proj2 (proj2 bigstep_to_steps)))).
 
 Fixpoint esize (a: expr) : nat :=
@@ -2708,28 +2708,28 @@ Qed.
 Lemma evalinf_funcall_steps:
   forall m fd args t k,
   evalinf_funcall m fd args t ->
-  forever_N step lt ge O (Callstate fd args k m) t.
+  forever_N (step ge) lt O (Callstate fd args k m) t.
 Proof.
   cofix COF.
 
   assert (COS:
     forall e m s t f k,
     execinf_stmt e m s t ->
-    forever_N step lt ge O (State f s k e m) t).
+    forever_N (step ge) lt O (State f s k e m) t).
   cofix COS.
 
   assert (COE:
     forall e m K a t C f k,
     evalinf_expr e m K a t ->
     leftcontext K RV C ->
-    forever_N step lt ge (esize a) (ExprState f (C a) k e m) t).
+    forever_N (step ge) lt (esize a) (ExprState f (C a) k e m) t).
   cofix COE.
 
   assert (COEL:
     forall e m a t C f k a1 al ty,
     evalinf_exprlist e m a t ->
     leftcontext RV RV C -> simple a1 = true -> simplelist al = true ->
-    forever_N step lt ge (esizelist a)
+    forever_N (step ge) lt (esizelist a)
                    (ExprState f (C (Ecall a1 (exprlist_app al a) ty)) k e m) t).
   cofix COEL.
   intros. inv H.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 272b929f1a..df992454c3 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -254,7 +254,7 @@ Qed.
 
 Lemma compat_eval_steps_aux f r e m r' m' s2 :
   simple r ->
-  star step ge s2 nil (ExprState f r' Kstop e m') ->
+  star (step ge) s2 nil (ExprState f r' Kstop e m') ->
   estep ge (ExprState f r Kstop e m) nil s2 ->
   exists r1,
     s2 = ExprState f r1 Kstop e m /\
@@ -283,7 +283,7 @@ Qed.
 
 Lemma compat_eval_steps:
   forall f r e m  r' m',
-  star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') ->
+  star (step ge) (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') ->
   simple r ->
   m' = m /\ compat_eval RV e r r' m.
 Proof.
@@ -308,7 +308,7 @@ Qed.
 
 Theorem eval_simple_steps:
   forall f r e m v ty m',
-  star step ge (ExprState f r Kstop e m) E0 (ExprState f (Eval v ty) Kstop e m') ->
+  star (step ge) (ExprState f r Kstop e m) E0 (ExprState f (Eval v ty) Kstop e m') ->
   simple r ->
   m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v.
 Proof.
@@ -468,7 +468,7 @@ Qed.
 
 Theorem constval_steps:
   forall f r m v v' ty m',
-  star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') ->
+  star (step ge) (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') ->
   constval ge r = OK v ->
   m' = m /\ ty = typeof r /\ Val.inject inj v v'.
 Proof.
@@ -595,7 +595,7 @@ Qed.
 Theorem transl_init_single_steps:
   forall ty a data f m v1 ty1 m' v chunk b ofs m'',
   transl_init_single ge ty a = OK data ->
-  star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
+  star (step ge) (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
   sem_cast v1 ty1 ty m' = Some v ->
   access_mode ty = By_value chunk ->
   Mem.store chunk m' b ofs v = Some m'' ->
@@ -761,8 +761,8 @@ Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) :=
 
 Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
   | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'',
-      star step ge (ExprState dummy_function a Kstop empty_env m)
-                E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
+      star (step ge) (ExprState dummy_function a Kstop empty_env m)
+                  E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
       sem_cast v1 ty1 ty m' = Some v ->
       access_mode ty = By_value chunk ->
       Mem.store chunk m' b ofs v = Some m'' ->
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index ee1df409d5..e53bacfb6a 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -813,8 +813,8 @@ Lemma step_makeif:
   forall f a s1 s2 k e le m v1 b,
   eval_expr tge e le m a v1 ->
   bool_val v1 (typeof a) m = Some b ->
-  star step1 tge (State f (makeif a s1 s2) k e le m)
-             E0 (State f (if b then s1 else s2) k e le m).
+  star (step1 tge) (State f (makeif a s1 s2) k e le m)
+                E0 (State f (if b then s1 else s2) k e le m).
 Proof.
   intros. functional induction (makeif a s1 s2).
 - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v.
@@ -883,8 +883,8 @@ Qed.
 
 Lemma push_seq:
   forall f sl k e le m,
-  star step1 tge (State f (makeseq sl) k e le m)
-              E0 (State f Sskip (Kseqlist sl k) e le m).
+  star (step1 tge) (State f (makeseq sl) k e le m)
+                E0 (State f Sskip (Kseqlist sl k) e le m).
 Proof.
   intros. unfold makeseq. generalize Sskip. revert sl k.
   induction sl; simpl; intros.
@@ -899,8 +899,8 @@ Lemma step_tr_rvalof:
   tr_rvalof ty a sl a' tmp ->
   typeof a = ty ->
   exists le',
-    star step1 tge (State f Sskip (Kseqlist sl k) e le m)
-                 t (State f Sskip k e le' m)
+    star (step1 tge) (State f Sskip (Kseqlist sl k) e le m)
+                   t (State f Sskip k e le' m)
   /\ eval_expr tge e le' m a' v
   /\ typeof a' = typeof a
   /\ forall x, ~In x tmp -> le'!x = le!x.
@@ -1430,8 +1430,8 @@ Lemma estep_simulation:
   forall S1 t S2, Cstrategy.estep ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
   exists S2',
-     (plus step1 tge S1' t S2' \/
-       (star step1 tge S1' t S2' /\ measure S2 < measure S1)%nat)
+     (plus (step1 tge) S1' t S2' \/
+       (star (step1 tge) S1' t S2' /\ measure S2 < measure S1)%nat)
   /\ match_states S2 S2'.
 Proof.
   induction 1; intros; inv MS.
@@ -1999,8 +1999,8 @@ Lemma sstep_simulation:
   forall S1 t S2, Csem.sstep ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
   exists S2',
-     (plus step1 tge S1' t S2' \/
-       (star step1 tge S1' t S2' /\ measure S2 < measure S1)%nat)
+     (plus (step1 tge) S1' t S2' \/
+       (star (step1 tge) S1' t S2' /\ measure S2 < measure S1)%nat)
   /\ match_states S2 S2'.
 Proof.
   induction 1; intros; inv MS.
@@ -2273,8 +2273,8 @@ Theorem simulation:
   forall S1 t S2, Cstrategy.step ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
   exists S2',
-     (plus step1 tge S1' t S2' \/
-       (star step1 tge S1' t S2' /\ measure S2 < measure S1)%nat)
+     (plus (step1 tge) S1' t S2' \/
+       (star (step1 tge) S1' t S2' /\ measure S2 < measure S1)%nat)
   /\ match_states S2 S2'.
 Proof.
   intros S1 t S2 STEP. destruct STEP.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 26d3d347cf..bc131fcb4f 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -314,8 +314,8 @@ Lemma step_Sset_debug:
   forall f id ty a k e le m v v',
   eval_expr tge e le m a v ->
   sem_cast v (typeof a) ty m = Some v' ->
-  plus step2 tge (State f (Sset_debug id ty a) k e le m)
-              E0 (State f Sskip k e (PTree.set id v' le) m).
+  plus (step2 tge) (State f (Sset_debug id ty a) k e le m)
+                E0 (State f Sskip k e (PTree.set id v' le) m).
 Proof.
   intros; unfold Sset_debug.
   assert (forall k, step2 tge (State f (Sset id (make_cast a ty)) k e le m)
@@ -334,8 +334,8 @@ Qed.
 Lemma step_add_debug_vars:
   forall f s e le m vars k,
   (forall id ty, In (id, ty) vars -> exists b, e!id = Some (b, ty)) ->
-  star step2 tge (State f (add_debug_vars vars s) k e le m)
-              E0 (State f s k e le m).
+  star (step2 tge) (State f (add_debug_vars vars s) k e le m)
+                E0 (State f s k e le m).
 Proof.
   unfold add_debug_vars. destruct (Compopts.debug tt).
 - induction vars; simpl; intros.
@@ -368,8 +368,8 @@ Lemma step_add_debug_params:
   list_norepet (var_names params) ->
   list_forall2 val_casted vl (map snd params) ->
   bind_parameter_temps params vl le1 = Some le ->
-  star step2 tge (State f (add_debug_params params s) k e le m)
-              E0 (State f s k e le m).
+  star (step2 tge) (State f (add_debug_params params s) k e le m)
+                E0 (State f s k e le m).
 Proof.
   unfold add_debug_params. destruct (Compopts.debug tt).
 - induction params as [ | [id ty] params ]; simpl; intros until le1; intros NR CAST BIND; inv CAST; inv NR.
@@ -1101,8 +1101,8 @@ Theorem store_params_correct:
   (forall id, ~In id (var_names params) -> tle2!id = tle1!id) ->
   (forall id, In id (var_names params) -> le!id = None) ->
   exists tle, exists tm',
-  star step2 tge (State f (store_params cenv params s) k te tle tm)
-              E0 (State f s k te tle tm')
+  star (step2 tge) (State f (store_params cenv params s) k te tle tm)
+                E0 (State f s k te tle tm')
   /\ bind_parameter_temps params targs tle2 = Some tle
   /\ Mem.inject j m' tm'
   /\ match_envs j cenv e le m' lo hi te tle tlo thi
@@ -2001,7 +2001,7 @@ End FIND_LABEL.
 
 Lemma step_simulation:
   forall S1 t S2, step1 ge S1 t S2 ->
-  forall S1' (MS: match_states S1 S1'), exists S2', plus step2 tge S1' t S2' /\ match_states S2 S2'.
+  forall S1' (MS: match_states S1 S1'), exists S2', plus (step2 tge) S1' t S2' /\ match_states S2 S2'.
 Proof.
   induction 1; simpl; intros; inv MS; simpl in *; try (monadInv TRS).
 
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 92bd708fef..432c379c7d 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -205,7 +205,7 @@ Qed.
 Lemma reacts_forever_reactive:
   exists T, Forever_reactive L s0 T.
 Proof.
-  exists (traceinf_of_traceinf' (build_traceinf' (star_refl (step L) (globalenv L) s0))).
+  exists (traceinf_of_traceinf' (build_traceinf' (star_refl (step L) s0))).
   apply reacts_forever_reactive_rec.
 Qed.
 
@@ -421,7 +421,7 @@ Lemma backward_simulation_forever_silent:
 Proof.
   assert (forall i s1 s2,
          Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 ->
-         forever_silent_N (step L1) order (globalenv L1) i s1).
+         forever_silent_N (step L1) order i s1).
     cofix COINDHYP; intros.
     inv H.  destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]].
     destruct A as [C | [C D]].
@@ -692,14 +692,11 @@ Unset Implicit Arguments.
 
 Section INF_SEQ_DECOMP.
 
-Variable genv: Type.
 Variable state: Type.
-Variable step: genv -> state -> trace -> state -> Prop.
-
-Variable ge: genv.
+Variable step: state -> trace -> state -> Prop.
 
 Inductive tstate: Type :=
-  ST: forall (s: state) (T: traceinf), forever step ge s T -> tstate.
+  ST: forall (s: state) (T: traceinf), forever step s T -> tstate.
 
 Definition state_of_tstate (S: tstate): state :=
   match S with ST s T F => s end.
@@ -708,7 +705,7 @@ Definition traceinf_of_tstate (S: tstate) : traceinf :=
 
 Inductive tstep: trace -> tstate -> tstate -> Prop :=
   | tstep_intro: forall s1 t T s2 S F,
-      tstep t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F))
+      tstep t (ST s1 (t *** T) (@forever_intro state step s1 t s2 T S F))
               (ST s2 T F).
 
 Inductive tsteps: tstate -> tstate -> Prop :=
@@ -748,7 +745,7 @@ Qed.
 
 Lemma tsteps_star:
   forall S1 S2, tsteps S1 S2 ->
-  exists t, star step ge (state_of_tstate S1) t (state_of_tstate S2)
+  exists t, star step (state_of_tstate S1) t (state_of_tstate S2)
          /\ traceinf_of_tstate S1 = t *** traceinf_of_tstate S2.
 Proof.
   induction 1.
@@ -761,7 +758,7 @@ Qed.
 
 Lemma tsilent_forever_silent:
   forall S,
-  tsilent S -> forever_silent step ge (state_of_tstate S).
+  tsilent S -> forever_silent step (state_of_tstate S).
 Proof.
   cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros.
   assert (tstep t (ST s1 (t *** T0) (forever_intro s1 t s0 f0))
@@ -777,7 +774,7 @@ Qed.
 
 Lemma treactive_forever_reactive:
   forall S,
-  treactive S -> forever_reactive step ge (state_of_tstate S) (traceinf_of_tstate S).
+  treactive S -> forever_reactive step (state_of_tstate S) (traceinf_of_tstate S).
 Proof.
   cofix COINDHYP; intros.
   destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply tsteps_refl.
@@ -786,7 +783,7 @@ Proof.
   apply forever_reactive_intro with s2.
   eapply star_right; eauto.
   red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction.
-  change (forever_reactive step ge (state_of_tstate (ST s2 T F)) (traceinf_of_tstate (ST s2 T F))).
+  change (forever_reactive step (state_of_tstate (ST s2 T F)) (traceinf_of_tstate (ST s2 T F))).
   apply COINDHYP.
   red; intros. apply H.
   eapply tsteps_trans. eauto.
@@ -795,15 +792,15 @@ Qed.
 
 Theorem forever_silent_or_reactive:
   forall s T,
-  forever step ge s T ->
-  forever_reactive step ge s T \/
+  forever step s T ->
+  forever_reactive step s T \/
   exists t, exists s', exists T',
-  star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'.
+  star step s t s' /\ forever_silent step s' /\ T = t *** T'.
 Proof.
   intros.
   destruct (treactive_or_tsilent (ST s T H)).
   left.
-  change (forever_reactive step ge (state_of_tstate (ST s T H)) (traceinf_of_tstate (ST s T H))).
+  change (forever_reactive step (state_of_tstate (ST s T H)) (traceinf_of_tstate (ST s T H))).
   apply treactive_forever_reactive. auto.
   destruct H0 as [S' [A B]].
   exploit tsteps_star; eauto. intros [t [C D]]. simpl in *.
diff --git a/common/Determinism.v b/common/Determinism.v
index 7fa01c2dad..4f8953d70a 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -514,11 +514,9 @@ Local Open Scope pair_scope.
 
 Definition world_sem : semantics := @Semantics_gen
   (state L * world)%type
-  (genvtype L)
-  (fun ge s t s' => step L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
+  (fun s t s' => step L s#1 t s'#1 /\ possible_trace s#2 t s'#2)
   (fun s => initial_state L s#1 /\ s#2 = initial_world)
   (fun s r => final_state L s#1 r)
-  (globalenv L)
   (symbolenv L).
 
 (** If the original semantics is determinate, the world-aware semantics is deterministic. *)
diff --git a/common/Smallstep.v b/common/Smallstep.v
index c269013bca..9437662752 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -32,67 +32,64 @@ Set Implicit Arguments.
 
 Section CLOSURES.
 
-Variable genv: Type.
 Variable state: Type.
 
 (** A one-step transition relation has the following signature.
-  It is parameterized by a global environment, which does not
-  change during the transition.  It relates the initial state
-  of the transition with its final state.  The [trace] parameter
-  captures the observable events possibly generated during the
-  transition. *)
+  It relates the initial state of the transition with its final state.
+  The [trace] parameter captures the observable events possibly
+  generated during the transition. *)
 
-Variable step: genv -> state -> trace -> state -> Prop.
+Variable step: state -> trace -> state -> Prop.
 
 (** No transitions: stuck state *)
 
-Definition nostep (ge: genv) (s: state) : Prop :=
-  forall t s', ~(step ge s t s').
+Definition nostep (s: state) : Prop :=
+  forall t s', ~(step s t s').
 
 (** Zero, one or several transitions.  Also known as Kleene closure,
     or reflexive transitive closure. *)
 
-Inductive star (ge: genv): state -> trace -> state -> Prop :=
+Inductive star: state -> trace -> state -> Prop :=
   | star_refl: forall s,
-      star ge s E0 s
+      star s E0 s
   | star_step: forall s1 t1 s2 t2 s3 t,
-      step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
-      star ge s1 t s3.
+      step s1 t1 s2 -> star s2 t2 s3 -> t = t1 ** t2 ->
+      star s1 t s3.
 
 Lemma star_one:
-  forall ge s1 t s2, step ge s1 t s2 -> star ge s1 t s2.
+  forall s1 t s2, step s1 t s2 -> star s1 t s2.
 Proof.
   intros. eapply star_step; eauto. apply star_refl. traceEq.
 Qed.
 
 Lemma star_two:
-  forall ge s1 t1 s2 t2 s3 t,
-  step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
-  star ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  step s1 t1 s2 -> step s2 t2 s3 -> t = t1 ** t2 ->
+  star s1 t s3.
 Proof.
   intros. eapply star_step; eauto. apply star_one; auto.
 Qed.
 
 Lemma star_three:
-  forall ge s1 t1 s2 t2 s3 t3 s4 t,
-  step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 ->
-  star ge s1 t s4.
+  forall s1 t1 s2 t2 s3 t3 s4 t,
+  step s1 t1 s2 -> step s2 t2 s3 -> step s3 t3 s4 -> t = t1 ** t2 ** t3 ->
+  star s1 t s4.
 Proof.
   intros. eapply star_step; eauto. eapply star_two; eauto.
 Qed.
 
 Lemma star_four:
-  forall ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
-  step ge s1 t1 s2 -> step ge s2 t2 s3 ->
-  step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
-  star ge s1 t s5.
+  forall s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
+  step s1 t1 s2 -> step s2 t2 s3 ->
+  step s3 t3 s4 -> step s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
+  star s1 t s5.
 Proof.
   intros. eapply star_step; eauto. eapply star_three; eauto.
 Qed.
 
 Lemma star_trans:
-  forall ge s1 t1 s2, star ge s1 t1 s2 ->
-  forall t2 s3 t, star ge s2 t2 s3 -> t = t1 ** t2 -> star ge s1 t s3.
+  forall s1 t1 s2, star s1 t1 s2 ->
+  forall t2 s3 t, star s2 t2 s3 -> t = t1 ** t2 -> star s1 t s3.
 Proof.
   induction 1; intros.
   rewrite H0. simpl. auto.
@@ -100,27 +97,27 @@ Proof.
 Qed.
 
 Lemma star_left:
-  forall ge s1 t1 s2 t2 s3 t,
-  step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
-  star ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  step s1 t1 s2 -> star s2 t2 s3 -> t = t1 ** t2 ->
+  star s1 t s3.
 Proof star_step.
 
 Lemma star_right:
-  forall ge s1 t1 s2 t2 s3 t,
-  star ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
-  star ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  star s1 t1 s2 -> step s2 t2 s3 -> t = t1 ** t2 ->
+  star s1 t s3.
 Proof.
   intros. eapply star_trans. eauto. apply star_one. eauto. auto.
 Qed.
 
 Lemma star_E0_ind:
-  forall ge (P: state -> state -> Prop),
+  forall (P: state -> state -> Prop),
   (forall s, P s s) ->
-  (forall s1 s2 s3, step ge s1 E0 s2 -> P s2 s3 -> P s1 s3) ->
-  forall s1 s2, star ge s1 E0 s2 -> P s1 s2.
+  (forall s1 s2 s3, step s1 E0 s2 -> P s2 s3 -> P s1 s3) ->
+  forall s1 s2, star s1 E0 s2 -> P s1 s2.
 Proof.
-  intros ge P BASE REC.
-  assert (forall s1 t s2, star ge s1 t s2 -> t = E0 -> P s1 s2).
+  intros P BASE REC.
+  assert (forall s1 t s2, star s1 t s2 -> t = E0 -> P s1 s2).
     induction 1; intros; subst.
     auto.
     destruct (Eapp_E0_inv _ _ H2). subst. eauto.
@@ -129,54 +126,54 @@ Qed.
 
 (** One or several transitions.  Also known as the transitive closure. *)
 
-Inductive plus (ge: genv): state -> trace -> state -> Prop :=
+Inductive plus: state -> trace -> state -> Prop :=
   | plus_left: forall s1 t1 s2 t2 s3 t,
-      step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
-      plus ge s1 t s3.
+      step s1 t1 s2 -> star s2 t2 s3 -> t = t1 ** t2 ->
+      plus s1 t s3.
 
 Lemma plus_one:
-  forall ge s1 t s2,
-  step ge s1 t s2 -> plus ge s1 t s2.
+  forall s1 t s2,
+  step s1 t s2 -> plus s1 t s2.
 Proof.
   intros. econstructor; eauto. apply star_refl. traceEq.
 Qed.
 
 Lemma plus_two:
-  forall ge s1 t1 s2 t2 s3 t,
-  step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
-  plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  step s1 t1 s2 -> step s2 t2 s3 -> t = t1 ** t2 ->
+  plus s1 t s3.
 Proof.
   intros. eapply plus_left; eauto. apply star_one; auto.
 Qed.
 
 Lemma plus_three:
-  forall ge s1 t1 s2 t2 s3 t3 s4 t,
-  step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 ->
-  plus ge s1 t s4.
+  forall s1 t1 s2 t2 s3 t3 s4 t,
+  step s1 t1 s2 -> step s2 t2 s3 -> step s3 t3 s4 -> t = t1 ** t2 ** t3 ->
+  plus s1 t s4.
 Proof.
   intros. eapply plus_left; eauto. eapply star_two; eauto.
 Qed.
 
 Lemma plus_four:
-  forall ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
-  step ge s1 t1 s2 -> step ge s2 t2 s3 ->
-  step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
-  plus ge s1 t s5.
+  forall s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
+  step s1 t1 s2 -> step s2 t2 s3 ->
+  step s3 t3 s4 -> step s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
+  plus s1 t s5.
 Proof.
   intros. eapply plus_left; eauto. eapply star_three; eauto.
 Qed.
 
 Lemma plus_star:
-  forall ge s1 t s2, plus ge s1 t s2 -> star ge s1 t s2.
+  forall s1 t s2, plus s1 t s2 -> star s1 t s2.
 Proof.
   intros. inversion H; subst.
   eapply star_step; eauto.
 Qed.
 
 Lemma plus_right:
-  forall ge s1 t1 s2 t2 s3 t,
-  star ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
-  plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  star s1 t1 s2 -> step s2 t2 s3 -> t = t1 ** t2 ->
+  plus s1 t s3.
 Proof.
   intros. inversion H; subst. simpl. apply plus_one. auto.
   rewrite Eapp_assoc. eapply plus_left; eauto.
@@ -184,24 +181,24 @@ Proof.
 Qed.
 
 Lemma plus_left':
-  forall ge s1 t1 s2 t2 s3 t,
-  step ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 ->
-  plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  step s1 t1 s2 -> plus s2 t2 s3 -> t = t1 ** t2 ->
+  plus s1 t s3.
 Proof.
   intros. eapply plus_left; eauto. apply plus_star; auto.
 Qed.
 
 Lemma plus_right':
-  forall ge s1 t1 s2 t2 s3 t,
-  plus ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
-  plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  plus s1 t1 s2 -> step s2 t2 s3 -> t = t1 ** t2 ->
+  plus s1 t s3.
 Proof.
   intros. eapply plus_right; eauto. apply plus_star; auto.
 Qed.
 
 Lemma plus_star_trans:
-  forall ge s1 t1 s2 t2 s3 t,
-  plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  plus s1 t1 s2 -> star s2 t2 s3 -> t = t1 ** t2 -> plus s1 t s3.
 Proof.
   intros. inversion H; subst.
   econstructor; eauto. eapply star_trans; eauto.
@@ -209,8 +206,8 @@ Proof.
 Qed.
 
 Lemma star_plus_trans:
-  forall ge s1 t1 s2 t2 s3 t,
-  star ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  star s1 t1 s2 -> plus s2 t2 s3 -> t = t1 ** t2 -> plus s1 t s3.
 Proof.
   intros. inversion H; subst.
   simpl; auto.
@@ -220,16 +217,16 @@ Proof.
 Qed.
 
 Lemma plus_trans:
-  forall ge s1 t1 s2 t2 s3 t,
-  plus ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
+  forall s1 t1 s2 t2 s3 t,
+  plus s1 t1 s2 -> plus s2 t2 s3 -> t = t1 ** t2 -> plus s1 t s3.
 Proof.
   intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto.
 Qed.
 
 Lemma plus_inv:
-  forall ge s1 t s2,
-  plus ge s1 t s2 ->
-  step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2.
+  forall s1 t s2,
+  plus s1 t s2 ->
+  step s1 t s2 \/ exists s', exists t1, exists t2, step s1 t1 s' /\ plus s' t2 s2 /\ t = t1 ** t2.
 Proof.
   intros. inversion H; subst. inversion H1; subst.
   left. rewrite E0_right. auto.
@@ -238,24 +235,24 @@ Proof.
 Qed.
 
 Lemma star_inv:
-  forall ge s1 t s2,
-  star ge s1 t s2 ->
-  (s2 = s1 /\ t = E0) \/ plus ge s1 t s2.
+  forall s1 t s2,
+  star s1 t s2 ->
+  (s2 = s1 /\ t = E0) \/ plus s1 t s2.
 Proof.
   intros. inv H. left; auto. right; econstructor; eauto.
 Qed.
 
 Lemma plus_ind2:
-  forall ge (P: state -> trace -> state -> Prop),
-  (forall s1 t s2, step ge s1 t s2 -> P s1 t s2) ->
+  forall (P: state -> trace -> state -> Prop),
+  (forall s1 t s2, step s1 t s2 -> P s1 t s2) ->
   (forall s1 t1 s2 t2 s3 t,
-   step ge s1 t1 s2 -> plus ge s2 t2 s3 -> P s2 t2 s3 -> t = t1 ** t2 ->
+   step s1 t1 s2 -> plus s2 t2 s3 -> P s2 t2 s3 -> t = t1 ** t2 ->
    P s1 t s3) ->
-  forall s1 t s2, plus ge s1 t s2 -> P s1 t s2.
+  forall s1 t s2, plus s1 t s2 -> P s1 t s2.
 Proof.
-  intros ge P BASE IND.
-  assert (forall s1 t s2, star ge s1 t s2 ->
-         forall s0 t0, step ge s0 t0 s1 ->
+  intros P BASE IND.
+  assert (forall s1 t s2, star s1 t s2 ->
+         forall s0 t0, step s0 t0 s1 ->
          P s0 (t0 ** t) s2).
   induction 1; intros.
   rewrite E0_right. apply BASE; auto.
@@ -265,30 +262,30 @@ Proof.
 Qed.
 
 Lemma plus_E0_ind:
-  forall ge (P: state -> state -> Prop),
-  (forall s1 s2 s3, step ge s1 E0 s2 -> star ge s2 E0 s3 -> P s1 s3) ->
-  forall s1 s2, plus ge s1 E0 s2 -> P s1 s2.
+  forall (P: state -> state -> Prop),
+  (forall s1 s2 s3, step s1 E0 s2 -> star s2 E0 s3 -> P s1 s3) ->
+  forall s1 s2, plus s1 E0 s2 -> P s1 s2.
 Proof.
   intros. inv H0. exploit Eapp_E0_inv; eauto. intros [A B]; subst. eauto.
 Qed.
 
 (** Counted sequences of transitions *)
 
-Inductive starN (ge: genv): nat -> state -> trace -> state -> Prop :=
+Inductive starN: nat -> state -> trace -> state -> Prop :=
   | starN_refl: forall s,
-      starN ge O s E0 s
+      starN O s E0 s
   | starN_step: forall n s t t1 s' t2 s'',
-      step ge s t1 s' -> starN ge n s' t2 s'' -> t = t1 ** t2 ->
-      starN ge (S n) s t s''.
+      step s t1 s' -> starN n s' t2 s'' -> t = t1 ** t2 ->
+      starN (S n) s t s''.
 
 Remark starN_star:
-  forall ge n s t s', starN ge n s t s' -> star ge s t s'.
+  forall n s t s', starN n s t s' -> star s t s'.
 Proof.
   induction 1; econstructor; eauto.
 Qed.
 
 Remark star_starN:
-  forall ge s t s', star ge s t s' -> exists n, starN ge n s t s'.
+  forall s t s', star s t s' -> exists n, starN n s t s'.
 Proof.
   induction 1.
   exists O; constructor.
@@ -297,15 +294,15 @@ Qed.
 
 (** Infinitely many transitions *)
 
-CoInductive forever (ge: genv): state -> traceinf -> Prop :=
+CoInductive forever: state -> traceinf -> Prop :=
   | forever_intro: forall s1 t s2 T,
-      step ge s1 t s2 -> forever ge s2 T ->
-      forever ge s1 (t *** T).
+      step s1 t s2 -> forever s2 T ->
+      forever s1 (t *** T).
 
 Lemma star_forever:
-  forall ge s1 t s2, star ge s1 t s2 ->
-  forall T, forever ge s2 T ->
-  forever ge s1 (t *** T).
+  forall s1 t s2, star s1 t s2 ->
+  forall T, forever s2 T ->
+  forever s1 (t *** T).
 Proof.
   induction 1; intros. simpl. auto.
   subst t. rewrite Eappinf_assoc.
@@ -318,28 +315,28 @@ Qed.
 Variable A: Type.
 Variable order: A -> A -> Prop.
 
-CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop :=
+CoInductive forever_N: A -> state -> traceinf -> Prop :=
   | forever_N_star: forall s1 t s2 a1 a2 T1 T2,
-      star ge s1 t s2 ->
+      star s1 t s2 ->
       order a2 a1 ->
-      forever_N ge a2 s2 T2 ->
+      forever_N a2 s2 T2 ->
       T1 = t *** T2 ->
-      forever_N ge a1 s1 T1
+      forever_N a1 s1 T1
   | forever_N_plus: forall s1 t s2 a1 a2 T1 T2,
-      plus ge s1 t s2 ->
-      forever_N ge a2 s2 T2 ->
+      plus s1 t s2 ->
+      forever_N a2 s2 T2 ->
       T1 = t *** T2 ->
-      forever_N ge a1 s1 T1.
+      forever_N a1 s1 T1.
 
 Hypothesis order_wf: well_founded order.
 
 Lemma forever_N_inv:
-  forall ge a s T,
-  forever_N ge a s T ->
+  forall a s T,
+  forever_N a s T ->
   exists t, exists s', exists a', exists T',
-  step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'.
+  step s t s' /\ forever_N a' s' T' /\ T = t *** T'.
 Proof.
-  intros ge a0. pattern a0. apply (well_founded_ind order_wf).
+  intros a0. pattern a0. apply (well_founded_ind order_wf).
   intros. inv H0.
   (* star case *)
   inv H1.
@@ -359,7 +356,7 @@ Proof.
 Qed.
 
 Lemma forever_N_forever:
-  forall ge a s T, forever_N ge a s T -> forever ge s T.
+  forall a s T, forever_N a s T -> forever s T.
 Proof.
   cofix COINDHYP; intros.
   destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]].
@@ -369,18 +366,18 @@ Qed.
 
 (** Yet another alternative definition of [forever]. *)
 
-CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop :=
+CoInductive forever_plus: state -> traceinf -> Prop :=
   | forever_plus_intro: forall s1 t s2 T1 T2,
-      plus ge s1 t s2 ->
-      forever_plus ge s2 T2 ->
+      plus s1 t s2 ->
+      forever_plus s2 T2 ->
       T1 = t *** T2 ->
-      forever_plus ge s1 T1.
+      forever_plus s1 T1.
 
 Lemma forever_plus_inv:
-  forall ge s T,
-  forever_plus ge s T ->
+  forall s T,
+  forever_plus s T ->
   exists s', exists t, exists T',
-  step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'.
+  step s t s' /\ forever_plus s' T' /\ T = t *** T'.
 Proof.
   intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2).
   split. auto.
@@ -390,7 +387,7 @@ Proof.
 Qed.
 
 Lemma forever_plus_forever:
-  forall ge s T, forever_plus ge s T -> forever ge s T.
+  forall s T, forever_plus s T -> forever s T.
 Proof.
   cofix COINDHYP; intros.
   destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]].
@@ -399,31 +396,31 @@ Qed.
 
 (** Infinitely many silent transitions *)
 
-CoInductive forever_silent (ge: genv): state -> Prop :=
+CoInductive forever_silent: state -> Prop :=
   | forever_silent_intro: forall s1 s2,
-      step ge s1 E0 s2 -> forever_silent ge s2 ->
-      forever_silent ge s1.
+      step s1 E0 s2 -> forever_silent s2 ->
+      forever_silent s1.
 
 (** An alternate definition. *)
 
-CoInductive forever_silent_N (ge: genv) : A -> state -> Prop :=
+CoInductive forever_silent_N: A -> state -> Prop :=
   | forever_silent_N_star: forall s1 s2 a1 a2,
-      star ge s1 E0 s2 ->
+      star s1 E0 s2 ->
       order a2 a1 ->
-      forever_silent_N ge a2 s2 ->
-      forever_silent_N ge a1 s1
+      forever_silent_N a2 s2 ->
+      forever_silent_N a1 s1
   | forever_silent_N_plus: forall s1 s2 a1 a2,
-      plus ge s1 E0 s2 ->
-      forever_silent_N ge a2 s2 ->
-      forever_silent_N ge a1 s1.
+      plus s1 E0 s2 ->
+      forever_silent_N a2 s2 ->
+      forever_silent_N a1 s1.
 
 Lemma forever_silent_N_inv:
-  forall ge a s,
-  forever_silent_N ge a s ->
+  forall a s,
+  forever_silent_N a s ->
   exists s', exists a',
-  step ge s E0 s' /\ forever_silent_N ge a' s'.
+  step s E0 s' /\ forever_silent_N a' s'.
 Proof.
-  intros ge a0. pattern a0. apply (well_founded_ind order_wf).
+  intros a0. pattern a0. apply (well_founded_ind order_wf).
   intros. inv H0.
   (* star case *)
   inv H1.
@@ -441,7 +438,7 @@ Proof.
 Qed.
 
 Lemma forever_silent_N_forever:
-  forall ge a s, forever_silent_N ge a s -> forever_silent ge s.
+  forall a s, forever_silent_N a s -> forever_silent s.
 Proof.
   cofix COINDHYP; intros.
   destruct (forever_silent_N_inv H) as [s' [a' [P Q]]].
@@ -451,15 +448,15 @@ Qed.
 
 (** Infinitely many non-silent transitions *)
 
-CoInductive forever_reactive (ge: genv): state -> traceinf -> Prop :=
+CoInductive forever_reactive: state -> traceinf -> Prop :=
   | forever_reactive_intro: forall s1 s2 t T,
-      star ge s1 t s2 -> t <> E0 -> forever_reactive ge s2 T ->
-      forever_reactive ge s1 (t *** T).
+      star s1 t s2 -> t <> E0 -> forever_reactive s2 T ->
+      forever_reactive s1 (t *** T).
 
 Lemma star_forever_reactive:
-  forall ge s1 t s2 T,
-  star ge s1 t s2 -> forever_reactive ge s2 T ->
-  forever_reactive ge s1 (t *** T).
+  forall s1 t s2 T,
+  star s1 t s2 -> forever_reactive s2 T ->
+  forever_reactive s1 (t *** T).
 Proof.
   intros. inv H0. rewrite <- Eappinf_assoc. econstructor.
   eapply star_trans; eauto.
@@ -475,11 +472,9 @@ End CLOSURES.
 
 Record semantics : Type := Semantics_gen {
   state: Type;
-  genvtype: Type;
-  step : genvtype -> state -> trace -> state -> Prop;
+  step : state -> trace -> state -> Prop;
   initial_state: state -> Prop;
   final_state: state -> int -> Prop;
-  globalenv: genvtype;
   symbolenv: Senv.t
 }.
 
@@ -491,21 +486,19 @@ Definition Semantics {state funtype vartype: Type}
                      (final_state: state -> int -> Prop)
                      (globalenv: Genv.t funtype vartype) :=
   {| state := state;
-     genvtype := Genv.t funtype vartype;
-     step := step;
+     step := step globalenv;
      initial_state := initial_state;
      final_state := final_state;
-     globalenv := globalenv;
      symbolenv := Genv.to_senv globalenv |}.
 
 (** Handy notations. *)
 
-Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope.
-Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope.
-Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope.
-Notation " 'Forever_silent' L " := (forever_silent (step L) (globalenv L)) (at level 1) : smallstep_scope.
-Notation " 'Forever_reactive' L " := (forever_reactive (step L) (globalenv L)) (at level 1) : smallstep_scope.
-Notation " 'Nostep' L " := (nostep (step L) (globalenv L)) (at level 1) : smallstep_scope.
+Notation " 'Step' L " := (step L) (at level 1) : smallstep_scope.
+Notation " 'Star' L " := (star (step L)) (at level 1) : smallstep_scope.
+Notation " 'Plus' L " := (plus (step L)) (at level 1) : smallstep_scope.
+Notation " 'Forever_silent' L " := (forever_silent (step L)) (at level 1) : smallstep_scope.
+Notation " 'Forever_reactive' L " := (forever_reactive (step L)) (at level 1) : smallstep_scope.
+Notation " 'Nostep' L " := (nostep (step L)) (at level 1) : smallstep_scope.
 
 Open Scope smallstep_scope.
 
@@ -759,7 +752,7 @@ Lemma simulation_forever_silent:
 Proof.
   assert (forall i s1 s2,
           Forever_silent L1 s1 -> match_states i s1 s2 ->
-          forever_silent_N (step L2) order (globalenv L2) i s2).
+          forever_silent_N (step L2) order i s2).
     cofix COINDHYP; intros.
     inv H. destruct (fsim_simulation S _ _ _ H1 _ _ H0) as [i' [s2' [A B]]].
     destruct A as [C | [C D]].
@@ -1374,17 +1367,17 @@ Inductive f2b_match_states: f2b_index -> state L1 -> state L2 -> Prop :=
   | f2b_match_before: forall s1 t s1' s2b s2 n s2a i,
       Step L1 s1 t s1' ->  t <> E0 ->
       Star L2 s2b E0 s2 ->
-      starN (step L2) (globalenv L2) n s2 t s2a ->
+      starN (step L2) n s2 t s2a ->
       match_states i s1 s2b ->
       f2b_match_states (F2BI_before n) s1 s2
   | f2b_match_after: forall n s2 s2a s1 i,
-      starN (step L2) (globalenv L2) (S n) s2 E0 s2a ->
+      starN (step L2) (S n) s2 E0 s2a ->
       match_states i s1 s2a ->
       f2b_match_states (F2BI_after (S n)) s1 s2.
 
 Remark f2b_match_after':
   forall n s2 s2a s1 i,
-  starN (step L2) (globalenv L2) n s2 E0 s2a ->
+  starN (step L2) n s2 E0 s2a ->
   match_states i s1 s2a ->
   f2b_match_states (F2BI_after n) s1 s2.
 Proof.
@@ -1536,24 +1529,22 @@ Variable L: semantics.
 
 Hypothesis Lwb: well_behaved_traces L.
 
-Inductive atomic_step (ge: genvtype L): (trace * state L) -> trace -> (trace * state L) -> Prop :=
+Inductive atomic_step: (trace * state L) -> trace -> (trace * state L) -> Prop :=
   | atomic_step_silent: forall s s',
       Step L s E0 s' ->
-      atomic_step ge (E0, s) E0 (E0, s')
+      atomic_step (E0, s) E0 (E0, s')
   | atomic_step_start: forall s ev t s',
       Step L s (ev :: t) s' ->
-      atomic_step ge (E0, s) (ev :: nil) (t, s')
+      atomic_step (E0, s) (ev :: nil) (t, s')
   | atomic_step_continue: forall ev t s,
       output_trace (ev :: t) ->
-      atomic_step ge (ev :: t, s) (ev :: nil) (t, s).
+      atomic_step (ev :: t, s) (ev :: nil) (t, s).
 
 Definition atomic : semantics := {|
   state := (trace * state L)%type;
-  genvtype := genvtype L;
   step := atomic_step;
   initial_state := fun s => initial_state L (snd s) /\ fst s = E0;
   final_state := fun s r => final_state L (snd s) r /\ fst s = E0;
-  globalenv := globalenv L;
   symbolenv := symbolenv L
 |}.
 
@@ -1806,6 +1797,6 @@ Record bigstep_sound (B: bigstep_semantics) (L: semantics) : Prop :=
     bigstep_diverges_sound:
       forall T,
       bigstep_diverges B T ->
-      exists s1, initial_state L s1 /\ forever (step L) (globalenv L) s1 T
+      exists s1, initial_state L s1 /\ forever (step L) s1 T
 }.
 
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 3aa87a4c10..b790dcf06e 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -74,7 +74,7 @@ Lemma exec_straight_exec:
   forall fb f c ep tf tc c' rs m rs' m',
   transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
   exec_straight tge tf tc rs m c' rs' m' ->
-  plus step tge (State rs m) E0 (State rs' m').
+  plus (step tge) (State rs m) E0 (State rs' m').
 Proof.
   intros. inv H.
   eapply exec_straight_steps_1; eauto.
@@ -401,7 +401,7 @@ Lemma exec_straight_steps:
     /\ agree ms2 sp rs2
     /\ (it1_is_parent ep i = true -> rs2#RAX = parent_sp s)) ->
   exists st',
-  plus step tge (State rs1 m1') E0 st' /\
+  plus (step tge) (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c ms2 m2) st'.
 Proof.
   intros. inversion H2. subst. monadInv H7.
@@ -425,7 +425,7 @@ Lemma exec_straight_steps_goto:
     /\ agree ms2 sp rs2
     /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
   exists st',
-  plus step tge (State rs1 m1') E0 st' /\
+  plus (step tge) (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c' ms2 m2) st'.
 Proof.
   intros. inversion H3. subst. monadInv H9.
@@ -468,7 +468,7 @@ Definition measure (s: Mach.state) : nat :=
 Theorem step_simulation:
   forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
-  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  (exists S2', plus (step tge) S1' t S2' /\ match_states S2 S2')
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
   induction 1; intros; inv MS.