(* This used to fail in Coq version 8.1 beta due to a non variable universe (issued by template polymorphism) being sent by
pretyping to the kernel (bug #1182) *)
Parameter T : Type. Parameter x : nat*nat.
Checklet (_, _) := x in sigT (fun _ : T => nat).
(* This used to raise an anomaly in V8.4, up to pl2 *)
Goal {x: nat & x=x}.
Fail exists (fun x => match
projT2 (projT2 x) as e in (_ = y) return _ = existT _ (projT1 x) (existT _ y e) with
| eq_refl => eq_refl end). Abort.
(* Some tests with ltac matching on building "if" and "let" *)
Goalforall b c d, (if negb b then c else d) = 0. intros. matchgoalwith
|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c) end. Abort.
Definition swap {A} {B} '((x,y):A*B) := (y,x).
Goalforall p, (let '(x,y) := swap p in x + y) = 0. intros. matchgoalwith
|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y) end. Abort.
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.
