|
(* Bad interaction between clear and the typability of ltac constr bindings *)
(* Original report *)
Goal 1 = 2.
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 => ltac:(let r := constr:(@eq Set x x) in
clear x;
exact r)) in
pose y
end.
(* Add extra test for typability (should not fail when bug closed) *)
Fail match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end.
Abort.
(* Second report raising a Not_found at the time of 21 Oct 2014 *)
Section F.
Variable x : nat.
Goal True.
evar (e : Prop).
assert e.
Fail let r := constr:(eq_refl x) in clear x; exact r.
Abort.
End F.
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
