diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 12:35:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 16:12:03 +0100 |
| commit | 34d52eb3577fa329e4637409e8d602fd23ac126d (patch) | |
| tree | bf37dc0e2e3f7ae706f5f4c6d3acf80f60631ae0 /test-suite/bugs/opened | |
| parent | c8721369d1d3e6572138fa7aab65e54f68459db4 (diff) | |
Test #3655 was failing due to an anomaly. Now it rather has to fail
normally, so failure is now detected by removing the "Fail".
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/3655.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3655.v b/test-suite/bugs/opened/3655.v index 2ec1da64d..841f77feb 100644 --- a/test-suite/bugs/opened/3655.v +++ b/test-suite/bugs/opened/3655.v @@ -2,4 +2,8 @@ Ltac bar x := pose x. Tactic Notation "foo" open_constr(x) := bar x. Class baz := { baz' : Type }. Goal True. - Fail foo baz'. +(* Original error was an anomaly which is fixed; now, it succeeds but + leaving an evar, while calling pose would not leave an evar, so I + guess it is still a bug in the sense that the semantics of pose is + not preserved *) + foo baz'. |