aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Util/Equality.v4
-rw-r--r--src/Util/ZUtil.v3
2 files changed, 4 insertions, 3 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 733b145c6..7657f96cb 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -41,7 +41,7 @@ Section gen.
Proof.
destruct H.
unfold decode.
- edestruct decode'.
+ edestruct (@decode' x _).
reflexivity.
Defined.
@@ -73,6 +73,6 @@ Section hprop.
intros x y p q.
pose proof (is_left_inv (@hprop_encode x y)) as H'.
rewrite <- (H' p), <- (H' q).
- apply f_equal, allpath_hprop.
+ apply f_equal; apply allpath_hprop.
Qed.
End hprop.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index b448406fc..eeb99188b 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1249,7 +1249,8 @@ Module Z.
End equiv_modulo.
Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *)
- Existing Instance equiv_modulo_Reflexive | 10.
+ Existing Instance equiv_modulo_Reflexive.
+ Existing Instance eq_Reflexive. (* prioritize [Reflexive eq] *)
Existing Instance equiv_modulo_Symmetric.
Existing Instance equiv_modulo_Transitive.
Existing Instance mul_mod_Proper.