Modify Classes/RelationClasses.v to compile with -mangle-names

The apply <- tactic was breaking, so we had to modify the definition
in Init/Tactics.v to use slightly fresher names.

2 files changed, 14 insertions, 13 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 9b92ade096..5381e91997 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -107,7 +107,7 @@ Section Defs.
   (** Any symmetric relation is equal to its inverse. *)
   
   Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
-  Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed.
+  Proof. hnf. intros x y H0. red in H0. apply symmetry. assumption. Qed.
 
   Section flip.
   
@@ -212,7 +212,7 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta
 Hint Extern 4 (subrelation (flip _) _) => 
   class_apply @subrelation_symmetric : typeclass_instances.
 
-Arguments irreflexivity {A R Irreflexive} [x] _.
+Arguments irreflexivity {A R Irreflexive} [x] _ : rename.
 Arguments symmetry {A} {R} {_} [x] [y] _.
 Arguments asymmetry {A} {R} {_} [x] [y] _ _.
 Arguments transitivity {A} {R} {_} [x] [y] [z] _ _.
@@ -260,7 +260,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ dintuition ]).
 
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [ simpl_relation ].
 
 (** Logical implication. *)
 
@@ -399,29 +399,30 @@ Program Instance predicate_equivalence_equivalence :
   Equivalence (@predicate_equivalence l).
 
   Next Obligation.
-    induction l ; firstorder.
+    intro l; induction l ; firstorder.
   Qed.
   Next Obligation.
-    induction l ; firstorder.
+    intro l; induction l ; firstorder.
   Qed.
   Next Obligation.
+    intro l.
     fold pointwise_lifting.
-    induction l.
+    induction l as [|T l IHl].
     - firstorder.
-    - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
+    - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)).
       firstorder.
   Qed.
 
 Program Instance predicate_implication_preorder :
   PreOrder (@predicate_implication l).
   Next Obligation.
-    induction l ; firstorder.
+    intro l; induction l ; firstorder.
   Qed.
   Next Obligation.
-    induction l.
+    intro l.
+    induction l as [|T l IHl].
     - firstorder.
-    - unfold predicate_implication in *. simpl in *.
-      intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+    - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)). firstorder.
   Qed.
 
 (** We define the various operations which define the algebra on binary relations,
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 6b4551318b..e1db68aea9 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -135,8 +135,8 @@ lazymatch T with
    rename H2 into H; find_equiv H |
    clear H]
 | forall x : ?t, _ =>
-  let a := fresh "a" with
-      H1 := fresh "H" in
+  let a := fresh "a" in
+  let H1 := fresh "H" in
     evar (a : t); pose proof (H a) as H1; unfold a in H1;
     clear a; clear H; rename H1 into H; find_equiv H
 | ?A <-> ?B => idtac