diff options
Diffstat (limited to 'test-suite/bugs/opened/4781.v')
-rw-r--r-- | test-suite/bugs/opened/4781.v | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v new file mode 100644 index 00000000..8b651ac2 --- /dev/null +++ b/test-suite/bugs/opened/4781.v @@ -0,0 +1,94 @@ +Ltac force_clear := + clear; + repeat match goal with + | [ H : _ |- _ ] => clear H + | [ H := _ |- _ ] => clearbody H + end. + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances. + +Goal True. +(* These work: *) + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + pose x. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := (eval cbv iota in (let v : T := x in v)) in + pose x. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(Set) with ?y => constr:(y) end in + pose x. +(* This fails with an error: *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => constr:(y) end in + pose x. (* The command has indeed failed with message: +Error: Variable y should be bound to a term. *) +(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x. + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := (eval cbv iota in x) in + pose x. + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := type of x in + pose x. (* should succeed *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:(_ : abstract_term term) in + let x := type of x in + pose x. (* should succeed *) + +(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time. + +Even stranger, consider:*) + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'. + let x := (eval cbv delta [x'] in x') in + pose x; + let z := (eval cbv iota in x) in + pose z. + +(*This works fine. But if I change the period to a semicolon, I get:*) + + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'; + let x := (eval cbv delta [x'] in x') in + pose x. (* Anomaly: Uncaught exception Not_found. Please report. *) + (* should succeed *) +(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) + + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'; + let x := (eval cbv delta [x'] in x') in + let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) + idtac. (* should succeed *) |