| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 331 B |
|
Quelle bug_10894.vSprache: Coq |
|||||||||||||||
|
(* Check that uconstrs are interpreted in the ltac-substituted environment *) (* Was a regression introduced in 4dab4fc (#7288) *) Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) := set (h := fun x => f). Fact test : nat -> nat. Proof. intros n. bind n in (n*n) as f. assert (f 0 = 0) by reflexivity. Abort.
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09