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.