diff options
| author |  Xavier Clerc <xavier.clerc@inria.fr> | 2014-11-25 15:41:48 +0100 |
|---|---|---|
| committer | Xavier Clerc <xavier.clerc@inria.fr> | 2014-11-25 15:41:48 +0100 |
| commit | ec9fda550cd997cc342e2f109cd6ceeadebec0e0 (patch) | |
| tree | ee0f8a717cf881319918ca9d26df2ea83cbec67d /test-suite | |
| parent | 87f9997244a9e0ac620343c9be1b7cb509818819 (diff) | |
Tweak some test cases.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/opened/3248.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3459.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3804.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v index 714df5cca..9e7d1eb5d 100644 --- a/test-suite/bugs/opened/3248.v +++ b/test-suite/bugs/opened/3248.v @@ -13,5 +13,5 @@ Proof. intros A B x y. pose (f := fun (x y : A) => conj x y). pose (a := $(ret_and_left f)$). - unify (a x y) (conj x y). + Fail unify (a x y) (conj x y). Abort. diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v index 7c0133099..9e6107b30 100644 --- a/test-suite/bugs/opened/3459.v +++ b/test-suite/bugs/opened/3459.v @@ -25,7 +25,7 @@ Variable x : nat. Goal True. evar (e : Prop). assert e. -let r := constr:(eq_refl x) in clear x; exact r. +Fail let r := constr:(eq_refl x) in clear x; exact r. Abort. End F. diff --git a/test-suite/bugs/opened/3804.v b/test-suite/bugs/opened/3804.v index 4c7f9344e..da9290cba 100644 --- a/test-suite/bugs/opened/3804.v +++ b/test-suite/bugs/opened/3804.v @@ -9,4 +9,4 @@ End Foo. Module Bar. Include Foo. End Bar. -Fail Definition foo := eq_refl : Foo.T = Bar.T. +Definition foo := eq_refl : Foo.T = Bar.T. |