Commit e6edf4f4 authored by Robbert Krebbers's avatar Robbert Krebbers

Make cofe_subst slightly stronger by not re-infering the type.

parent ce748a67
......@@ -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} := {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment