4 files changed, 14 insertions, 6 deletions
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index 61e911678..ef1737bf8 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -7,3 +7,11 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.7 *)
+
+(* In 8.7, omega wasn't taking advantage of local abbreviations,
+   see bug 148 and PR#768. For adjusting this flag, we're forced to
+   first dynlink the omega plugin, but we should avoid doing a full
+   "Require Omega", since it has some undesired effects (at least on hints)
+   and breaks at least fiat-crypto. *)
+Declare ML Module "omega_plugin".
+Unset Omega UseLocalDefs.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 25b042ca9..0041bfa1c 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -762,7 +762,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
   Qed.
 
-  Add Morphism cardinal : cardinal_m.
+  Add Morphism cardinal with signature (Equal ==> Logic.eq) as cardinal_m.
   Proof.
   exact Equal_cardinal.
   Qed.
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 886533586..87b7a9a3b 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -27,7 +27,7 @@ Local Ltac simplif flags :=
       | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id
       | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
     (* generalize (id0 id1); intro; clear id0 does not work
-       (see Marco Maggiesi's bug PR#301)
+       (see Marco Maggiesi's BZ#301)
     so we instead use Assert and exact. *)
     assert X2; [exact (id0 id1) | clear id0]
       | id: forall (_ : ?X1), ?X2|- _ =>
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 88e1298fb..5d055b547 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -101,7 +101,7 @@ Proof.
  - apply Qred_complete.
 Qed.
 
-Add Morphism Qred : Qred_comp.
+Add Morphism Qred with signature (Qeq ==> Qeq) as Qred_comp.
 Proof.
   intros. now rewrite !Qred_correct.
 Qed.
@@ -125,19 +125,19 @@ Proof.
   intros; unfold Qminus'; apply Qred_correct; auto.
 Qed.
 
-Add Morphism Qplus' : Qplus'_comp.
+Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp.
 Proof.
   intros; unfold Qplus'.
   rewrite H, H0; auto with qarith.
 Qed.
 
-Add Morphism Qmult' : Qmult'_comp.
+Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp.
 Proof.
   intros; unfold Qmult'.
   rewrite H, H0; auto with qarith.
 Qed.
 
-Add Morphism Qminus' : Qminus'_comp.
+Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp.
 Proof.
   intros; unfold Qminus'.
   rewrite H, H0; auto with qarith.