Imported Upstream version 8.6upstream/8.6

5 files changed, 22 insertions, 17 deletions

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index c41eb2fa..1cfca416 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -452,7 +452,7 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     end
   in
@@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive
 Section Normalize.
   Context (A : Type).
 
-  Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+  Class Normalizes (m : crelation A) (m' : crelation A) :=
     normalizes : relation_equivalence m m'.
   
   (** Current strategy: add [flip] everywhere and reduce using [subrelation]
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index c4588947..80b0b7e4 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1.
 
-Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1.
 
-Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
 
   Next Obligation.
   Proof. intros A R sa x y z Hxy Hyz.
@@ -123,7 +123,7 @@ Section Respecting.
 
 End Respecting.
 
-(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+(** The default equivalence on function spaces, with higher priority than [eq]. *)
 
 Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
   Reflexive (pointwise_relation A eqB) | 9.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8d942d90..06511ace 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -465,12 +465,12 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     end
   in
   let rec do_partial H ar m := 
-    match ar with
+    lazymatch ar with
       | 0%nat => do_partial_apps H m ltac:(fail 1)
       | S ?n' =>
         match m with
@@ -483,7 +483,7 @@ Ltac partial_application_tactic :=
      let n := fresh in evar (n:nat) ;
      let v := eval compute in n in clear n ;
       let H := fresh in
-        assert(H:Params m' v) by typeclasses eauto ;
+        assert(H:Params m' v) by (subst m'; once typeclasses eauto) ;
           let v' := eval compute in v in subst m';
             (sk H v' || fail 1))
     || fk
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index cbde5f9a..8d1c4982 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -43,6 +43,9 @@ Generalizable Variables A B RA RB Ri Ro f.
 Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A :=
  fun a a' => R (f a) (f a').
 
+(** Instances on RelCompFun must match syntactically *)
+Typeclasses Opaque RelCompFun. 
+
 Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
 
 Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope.
@@ -65,6 +68,8 @@ Instance snd_measure : @Measure (A * B) B Snd.
 Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
  relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).
 
+Typeclasses Opaque RelProd.
+
 Infix "*" := RelProd : signature_scope.
 
 Section RelCompFun_Instances.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 145d451f..190397ae 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "by" tactic3(t) :=
-  setoidreplace (default_relation x y) ltac:t.
+  setoidreplace (default_relation x y) ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceat (default_relation x y) ltac:t o.
+  setoidreplaceat (default_relation x y) ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id)
   "by" tactic3(t) :=
-  setoidreplacein (default_relation x y) id ltac:t.
+  setoidreplacein (default_relation x y) id ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceinat (default_relation x y) id ltac:t o.
+  setoidreplaceinat (default_relation x y) id ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel) :=
@@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "by" tactic3(t) :=
-  setoidreplace (rel x y) ltac:t.
+  setoidreplace (rel x y) ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceat (rel x y) ltac:t o.
+  setoidreplaceat (rel x y) ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
@@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "by" tactic3(t) :=
-  setoidreplacein (rel x y) id ltac:t.
+  setoidreplacein (rel x y) id ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceinat (rel x y) id ltac:t o.
+  setoidreplaceinat (rel x y) id ltac:(t) o.
 
 (** The [add_morphism_tactic] tactic is run at each [Add Morphism]
    command before giving the hand back to the user to discharge the