From 34d52eb3577fa329e4637409e8d602fd23ac126d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 8 Nov 2014 12:35:53 +0100 Subject: Test #3655 was failing due to an anomaly. Now it rather has to fail normally, so failure is now detected by removing the "Fail". --- test-suite/bugs/opened/3655.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'test-suite/bugs/opened') 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'. -- cgit v1.2.3