diff options
| -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 2ec1da64d4..841f77febb 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'. |