From e6edf4f46c245cd53de3d08a0154933b274b4bec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Dec 2015 11:44:13 +0100
Subject: [PATCH] Make cofe_subst slightly stronger by not re-infering the
type.
---
modures/cofe.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/modures/cofe.v b/modures/cofe.v
index 15b23fe8b..2692e0b03 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -11,8 +11,8 @@ Hint Extern 0 (_ ={_}= _) => symmetry; assumption.
Ltac cofe_subst :=
repeat match goal with
| _ => progress simplify_equality'
- | H: @dist _ ?d ?n ?x _ |- _ => setoid_subst_aux (@dist _ d n) x
- | H: @dist _ ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist _ d n) x
+ | H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x
+ | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end.
Record chain (A : Type) `{Dist A} := {
--
GitLab