diff options
| author | Pierre-Marie Pédrot | 2014-09-08 22:05:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-08 22:05:50 +0200 |
| commit | 9fb15a33ba59b3543e1d277d7bf4b6bd2f69922d (patch) | |
| tree | dd4d14a281ec2e5cba1f9501dfca2492f1a30219 | |
| parent | c310dc5efedcbc31d74d568e5bb4bfecf458c25b (diff) | |
Fixing TestRefine test-suite file.
| -rw-r--r-- | test-suite/success/TestRefine.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 213b528301..5bea53c947 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -53,7 +53,7 @@ Abort. Lemma essai2 : forall x : nat, x = x. - refine (fix f (x : nat) : x = x := _). +Fail refine (fix f (x : nat) : x = x := _). Restart. |