diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/6323.v | 9 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 4 |
2 files changed, 11 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/6323.v b/test-suite/bugs/closed/6323.v new file mode 100644 index 0000000000..fdc33befc6 --- /dev/null +++ b/test-suite/bugs/closed/6323.v @@ -0,0 +1,9 @@ +Goal True. + simple refine (let X : Type := _ in _); + [ abstract exact Set using Set' + | let X' := (eval cbv delta [X] in X) in + clear X; + simple refine (let id' : { x : X' | True } -> X' := _ in _); + [ abstract refine (@proj1_sig _ _) | ] + ]. +Abort. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index c5d58ec1ec..eb9f571022 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,7 +1,7 @@ The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := - symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. @@ -32,7 +32,7 @@ nat 0 0 Ltac foo := - let x := intros ** in + let x := intros in let y := intros -> in let v := constr:(nil) in let w := () in |