diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2139.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2139.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v index 4f71d097f..415a1b27d 100644 --- a/test-suite/bugs/closed/shouldsucceed/2139.v +++ b/test-suite/bugs/closed/shouldsucceed/2139.v @@ -2,19 +2,19 @@ Class Patch (patch : Type) := { commute : patch -> patch -> Prop -}. - +}. + Parameter flip : forall `{patchInstance : Patch patch} - {a b : patch}, + {a b : patch}, commute a b <-> commute b a. - + Lemma Foo : forall `{patchInstance : Patch patch} - {a b : patch}, + {a b : patch}, (commute a b) -> True. -Proof. -intros. -apply flip in H. +Proof. +intros. +apply flip in H. (* failed in well-formed arity check because elimination predicate of iff in (@flip _ _ _ _) had normalized evars while the ones in the |