| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 802 B |
|
Quelle bug_2310.v Sprache: Coq |
|||||||||
|
(* Dependent higher-order hole in "refine" (simplified version) *)
Set Implicit Arguments. Inductive Nest t := Cons : Nest (prod t t) -> Nest t. Definition cast A x y Heq P H := @eq_rect A x P H y Heq. Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. (* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta. It raises a regular error in 8.3 and almost succeeds with the new proof engine: there are two solutions to a unification problem (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either leave P as subgoal or choose itself one solution *) intros. Fail refine (Cons (cast H _ y)). Unset Solve Unification Constraints. (* Keep the unification constraint around *) refine (Cons (cast H _ y)). intros. refine (Nest (prod X X)). Qed. ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28