Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_3459.v Sprache: Coq

Original von: Coq^©

(* 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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.