diff --git a/erasure/theories/EAst.v b/erasure/theories/EAst.v
index 2ea94d006..164dd8e3c 100644
--- a/erasure/theories/EAst.v
+++ b/erasure/theories/EAst.v
@@ -27,21 +27,20 @@ Definition test_def {term : Set} (f : term -> bool) (d : def term) :=
 Definition mfixpoint (term : Set) := list (def term).
 
 Inductive term : Set :=
-| tBox       : term (* Represents all proofs *)
-| tRel       : nat -> term
-| tVar       : ident -> term (* For free variables (e.g. in a goal) *)
-| tEvar      : nat -> list term -> term
-| tLambda    : name -> term -> term
-| tLetIn     : name -> term (* the term *) -> term -> term
-| tApp       : term -> term -> term
-| tConst     : kername -> term
-| tConstruct : inductive -> nat -> list term -> term
-| tCase      : (inductive * nat) (* # of parameters *) ->
-               term (* discriminee *) -> list (list name * term) (* branches *) -> term
-| tProj      : projection -> term -> term
-| tFix       : mfixpoint term -> nat -> term
-| tCoFix     : mfixpoint term -> nat -> term
-| tPrim      : prim_val term -> term.
+| tBox (* Represents all proofs *)
+| tRel (n : nat)
+| tVar (i : ident) (* For free variables (e.g. in a goal) *)
+| tEvar (n : nat) (l : list term)
+| tLambda (na : name) (t : term)
+| tLetIn (na : name) (b t : term) (* let na := b : B in t *)
+| tApp (u v : term)
+| tConst (k : kername)
+| tConstruct (ind : inductive) (n : nat) (args : list term)
+| tCase (indn : inductive * nat (* # of parameters *)) (c : term  (* discriminee *)) (brs : list (list name * term) (* branches *))
+| tProj (p : projection) (c : term)
+| tFix (mfix : mfixpoint term) (idx : nat)
+| tCoFix (mfix : mfixpoint term) (idx : nat)
+| tPrim (prim : prim_val term).
 
 Derive NoConfusion for term.
 
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index 1fc9a4ab7..78dab5e91 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -1172,7 +1172,7 @@ Proof.
     solve_all. clear -X0. eapply All2_All2_Set. solve_all.
     match goal with H : _ |- _ => apply H end.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
-    cbn -[lookup_constructor] in H |- *. destruct l => //.
+    cbn -[lookup_constructor] in H |- *. destruct args => //.
     destruct lookup_constructor eqn:hl => //.
     destruct p as [[mdecl idecl] cdecl].
     eapply eval_construct_block => //.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
index b322d74d8..1a1469ad1 100644
--- a/erasure/theories/EImplementBox.v
+++ b/erasure/theories/EImplementBox.v
@@ -578,5 +578,5 @@ Proof.
     eapply All2_All2_Set.
     solve_all. now destruct b.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
-    cbn -[lookup_constructor] in H |- *. destruct l => //.
+    cbn -[lookup_constructor] in H |- *. destruct args => //.
 Qed.
diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v
index 65380d912..87d535a5e 100644
--- a/erasure/theories/EInduction.v
+++ b/erasure/theories/EInduction.v
@@ -47,24 +47,24 @@ Proof.
   fix auxl' 1.
   destruct l; constructor; [|apply auxl'].
   apply auxt.
-  revert l.
+  revert args.
   fix auxl' 1.
-  destruct l; constructor; [|apply auxl'].
+  destruct args; constructor; [|apply auxl'].
   apply auxt.
 
-  revert l.
+  revert brs.
   fix auxl' 1.
-  destruct l; constructor; [|apply auxl'].
+  destruct brs; constructor; [|apply auxl'].
   apply auxt.
 
-  revert m.
+  revert mfix.
   fix auxm 1.
-  destruct m; constructor; [|apply auxm].
+  destruct mfix; constructor; [|apply auxm].
   apply auxt.
 
-  revert m.
+  revert mfix.
   fix auxm 1.
-  destruct m; constructor; [|apply auxm].
+  destruct mfix; constructor; [|apply auxm].
   apply auxt.
 Defined.
 
diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v
index 1772da104..0eaa0b364 100644
--- a/erasure/theories/EInlineProjections.v
+++ b/erasure/theories/EInlineProjections.v
@@ -720,7 +720,7 @@ Proof.
     all:constructor; eauto.
     cbn [atom optimize] in i |- *.
     rewrite -lookup_constructor_optimize //.
-    destruct l; cbn in *; eauto.
+    destruct args; cbn in *; eauto.
 Qed.
 
 From MetaCoq.Erasure Require Import EEtaExpanded.
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index 0bbc6b016..38cc0bbf5 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -726,7 +726,7 @@ Proof.
         destruct v => /= //.
   - destruct t => //.
     all:constructor; eauto. cbn [atom remove_match_on_box] in i |- *.
-    rewrite -lookup_constructor_remove_match_on_box //. destruct l => //.
+    rewrite -lookup_constructor_remove_match_on_box //. destruct args => //.
 Qed.
 
 From MetaCoq.Erasure Require Import EEtaExpanded.
diff --git a/erasure/theories/EReflect.v b/erasure/theories/EReflect.v
index be00e2178..69f9ebaba 100644
--- a/erasure/theories/EReflect.v
+++ b/erasure/theories/EReflect.v
@@ -61,7 +61,7 @@ Proof.
   - destruct (IHx1 t1) ; nodec.
     destruct (IHx2 t2) ; nodec.
     subst. left. reflexivity.
-  - revert l. induction X ; intro l0.
+  - revert args0. induction X ; intro l0.
     + destruct l0.
       * left. reflexivity.
       * right. discriminate.
@@ -71,7 +71,7 @@ Proof.
         destruct (p t) ; nodec.
         inversion e. subst; left; reflexivity.
   - destruct (IHx t) ; nodec.
-    subst. revert l0. clear IHx.
+    subst. revert brs. clear IHx.
     induction X ; intro l0.
     + destruct l0.
       * left. reflexivity.
@@ -79,14 +79,14 @@ Proof.
     + destruct l0.
       * right. discriminate.
       * destruct (IHX l0) ; nodec.
-        destruct (p (snd p1)) ; nodec.
-        destruct (eq_dec (fst x) (fst p1)) ; nodec.
-        destruct x, p1.
+        destruct (p (snd p0)) ; nodec.
+        destruct (eq_dec (fst x) (fst p0)) ; nodec.
+        destruct x, p0.
         left.
         cbn in *. subst. inversion e. reflexivity.
   - destruct (IHx t) ; nodec.
     left. subst. reflexivity.
-  - revert m0. induction X ; intro m0.
+  - revert mfix. induction X ; intro m0.
     + destruct m0.
       * left. reflexivity.
       * right. discriminate.
@@ -99,7 +99,7 @@ Proof.
         subst. inversion e0. subst.
         destruct (eq_dec rarg rarg0) ; nodec.
         subst. left. reflexivity.
-  - revert m0. induction X ; intro m0.
+  - revert mfix. induction X ; intro m0.
     + destruct m0.
       * left. reflexivity.
       * right. discriminate.
@@ -112,7 +112,7 @@ Proof.
         subst. inversion e0. subst.
         destruct (eq_dec rarg rarg0) ; nodec.
         subst. left. reflexivity.
-  - destruct (eq_dec p p0); nodec.
+  - destruct (eq_dec p prim); nodec.
     left; subst. reflexivity.
 Defined.
 
diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v
index 75ee2581a..04aa58256 100644
--- a/erasure/theories/EWcbvEval.v
+++ b/erasure/theories/EWcbvEval.v
@@ -1426,7 +1426,7 @@ Section WcbvEnv.
     eauto using extends_lookup_constructor.
     clear -a iha. induction a; constructor; eauto. apply iha. apply IHa, iha.
     constructor.
-    destruct t => //. cbn [atom] in i. destruct l => //. destruct lookup_constructor eqn:hl => //.
+    destruct t => //. cbn [atom] in i. destruct args => //. destruct lookup_constructor eqn:hl => //.
     eapply (extends_lookup_constructor wf ex) in hl. now cbn [atom].
     cbn in i. now rewrite andb_false_r in i.
   Qed.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
index 5daa7f13d..1ac8603df 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
@@ -569,7 +569,7 @@ Proof.
     constructor => //; rtoProp; intuition auto.
     move/andP: H => [] /andP[] has isl hf => //.
     eapply on_cstr => //. destruct cstr_as_blocks.
-    rtoProp; intuition auto. solve_all. destruct l => //.
+    rtoProp; intuition auto. solve_all. destruct args => //.
     eapply on_case; rtoProp; intuition auto. solve_all.
     eapply on_proj; rtoProp; intuition auto.
     rtoProp; intuition auto.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
index 3bd5cda4d..f7b7d4325 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
@@ -463,7 +463,7 @@ Proof.
     constructor => //; rtoProp; intuition auto.
     move/andP: H => [] /andP[] has isl hf => //.
     eapply on_cstr => //. destruct cstr_as_blocks.
-    rtoProp; intuition auto. solve_all. destruct l => //.
+    rtoProp; intuition auto. solve_all. destruct args => //.
     eapply on_case; rtoProp; intuition auto. solve_all.
     eapply on_proj; rtoProp; intuition auto.
     rtoProp; intuition auto.
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index 9dc6e0310..3d7b415c7 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -722,7 +722,7 @@ Proof.
     eapply on_letin; rtoProp; intuition auto.
     eapply on_app; rtoProp; intuition auto.
     constructor; cbn; auto. rewrite cstbl in H0.
-    destruct l => //. constructor => //.
+    destruct args => //. constructor => //.
     eapply on_case; rtoProp; intuition auto. ELiftSubst.solve_all.
     eapply on_proj; auto.
     eapply on_fix; eauto. move/andP: H0 => [] _ wf. solve_all.
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index 044e57def..1d63a9aa9 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -1795,7 +1795,7 @@ Proof.
 
       edestruct s2 as (v'' & IH1'' & IH2'').
 
-      eapply represents_substl_rev with (vs := _ :: fix_env vfix E0) (nms := na0 :: List.rev (map fst vfix)); eauto. (* having represents_substl_rev with nms ++ Gamma created an order problem here. changing it there fixes the problem here. but is this correct? *)
+      eapply represents_substl_rev with (vs := _ :: fix_env vfix E0) (nms := na1 :: List.rev (map fst vfix)); eauto. (* having represents_substl_rev with nms ++ Gamma created an order problem here. changing it there fixes the problem here. but is this correct? *)
       8:{ eexists. split. eauto.
           eapply eval_fix_unfold; eauto.
           solve_all.
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index c82ab3dd8..40c158195 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -2601,7 +2601,7 @@ Proof.
   destruct f; try solve [now econstructor].
   - easy.
   - cbn in *.
-    destruct p.
+    destruct indn.
     eapply dearg_spec_case.
   - cbn in *.
     destruct p.
@@ -4335,15 +4335,15 @@ Proof.
     all : eauto.
   - eapply eval_atom.
     depelim t;auto.
-    destruct l;simpl in *;try congruence.
+    destruct args;simpl in *;try congruence.
     propify.
-    destruct i0.
+    destruct i.
     destruct (EGlobalEnv.lookup_constructor (trans_env Σ) _ _) as [p | ] eqn:He;simpl in *;try congruence.
     destruct p as [[??]?].
     apply lookup_ctor_trans_env in He as ee.
     destruct ee as (mib & oib & ctor & Hc & Hmib & Hoib & Hctor).
     subst.
-    destruct ctor as [[ind m] l0].
+    destruct ctor as [[? ?] ?].
     eapply lookup_constructor_debox_types in Hc.
     eapply lookup_ctor_trans_env_inv in Hc;eauto.
     now rewrite Hc.
diff --git a/erasure/theories/Typed/TypeAnnotations.v b/erasure/theories/Typed/TypeAnnotations.v
index e6b195cd1..f37c98f9e 100644
--- a/erasure/theories/Typed/TypeAnnotations.v
+++ b/erasure/theories/Typed/TypeAnnotations.v
@@ -557,7 +557,7 @@ Proof.
     exact (ta.1, f _ All_nil _ ta.2.2).
   - exact (annot_dearg_single _ ta argsa).
   - exact (annot_dearg_single _ ta argsa).
-  - destruct p.
+  - destruct indn.  
     refine (annot_mkApps _ argsa).
     cbn in *.
     refine (ta.1, _).
@@ -708,7 +708,7 @@ Module AnnotOptimizePropDiscr.
     - exact (a.1, f _ a.2).
     - exact (a.1, (f _ a.2.1, f _ a.2.2)).
     - exact (a.1, (f _ a.2.1, f _ a.2.2)).
-    - assert (br_annots : bigprod (fun br => annots box_type br.2) (map (on_snd (remove_match_on_box Σ)) l)).
+    - assert (br_annots : bigprod (fun br => annots box_type br.2) (map (on_snd (remove_match_on_box Σ)) brs)).
       { refine (bigprod_map _ a.2.2).
         intros ? a'; apply (f _ a'). }
       unfold isprop_ind.
@@ -724,7 +724,7 @@ Module AnnotOptimizePropDiscr.
          to a substitution of boxes into f
          (f[tBox/a1,..,tBox/an]) *)
       destruct br_annots as (fa&_).
-      revert l0 t0 fa.
+      revert l t fa.
       clear.
       fix f 1.
       intros [] hd hda.