diff options
Diffstat (limited to 'test-suite/bugs/opened/3459.v')
| -rw-r--r-- | test-suite/bugs/opened/3459.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v index 9e6107b3..762611f7 100644 --- a/test-suite/bugs/opened/3459.v +++ b/test-suite/bugs/opened/3459.v @@ -7,9 +7,9 @@ Proof. (* This line used to fail with a Not_found up to some point, and then to produce an ill-typed term *) match goal with - | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in + | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in clear x; - exact r)$) in + exact r)) in pose y end. (* Add extra test for typability (should not fail when bug closed) *) |