3 files changed, 7 insertions, 7 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 27e1ca8444..a349eb9085 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -238,8 +238,8 @@ Ltac inject_left H :=
 Ltac inject_right H :=
   progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H.
 
-Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
-Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
+Ltac autoinjections_left := repeat autoinjection ltac:(inject_left).
+Ltac autoinjections_right := repeat autoinjection ltac:(inject_right).
 
 Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
   simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
@@ -333,7 +333,7 @@ Ltac simplify_one_dep_elim_term c :=
       (let hyp := fresh in intros hyp ;
         move hyp before y ; revert_until hyp ; generalize dependent y ;
           refine (solution_right _ _ _ _)(*  ; intros until 0 *))
-    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; exfalso ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 66ca3e577d..dfd6b0eae0 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -252,7 +252,7 @@ Ltac autoinjection tac :=
 
 Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H.
 
-Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject).
+Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)).
 
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)
 
@@ -264,7 +264,7 @@ Ltac bang :=
   match goal with
     | |- ?x =>
       match x with
-        | appcontext [False_rect _ ?p] => elim p
+        | context [False_rect _ ?p] => elim p
       end
   end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 154200d769..c490ea5166 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -89,7 +89,7 @@ Section Measure_well_founded.
   Lemma measure_wf: well_founded MR.
   Proof with auto.
     unfold well_founded.
-    cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a).
+    cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
       intros.
       apply (H (m a))...
     apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+        context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end