Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/     Datei vom 4.1.2008 mit Größe 928 B image not shown  

Impressum remember.v   Interaktion und
Portierbarkeitunbekannt

 
(* Testing remember and co *)

Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
intros.
Fail remember nat as X.
Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
Fail remember nat as X.
Abort.

(* Testing Ltac interpretation of remember (was not working up to r16181) *)

Goal (1 + 2 + 3 = 6).
let name := fresh "fresh" in
remember (1 + 2) as x eqn:name.
rewrite fresh.
Abort.

(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
                  
Module A.
Axiom N : nat.
End A.
Module B.
Include A.
End B.
Goal id A.N = B.N.
reflexivity.
Qed.           
                

100%


[ Seitenstruktur0.11Drucken  etwas mehr zur Ethik  ]