some qed-

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index a3858dfb749a73c58c48cebbf53e5e2a93807b14..bf3bae3a8dc7cb45142b8c2c4657e7953808878c 100644 (file)
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -1,4 +1,4 @@
-(*
+ (*
     ||M||  This file is part of HELM, an Hypertextual, Electronic        
     ||A||  Library of Mathematics, developed at the Computer Science     
     ||T||  Department of the University of Bologna, Italy.                     
@@ -47,7 +47,7 @@ theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y →
 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
 
 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
-#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed-.
 
 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
@@ -56,7 +56,7 @@ theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
 #A #B #Ha #Heq (elim Heq); //; qed.
 
 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
-#A #x #y #z #H1 #H2 >H1; //; qed.
+#A #x #y #z #H1 #H2 >H1; //; qed-.
 
 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
 #A #B #f #x #y #H >H; //; qed.

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index b31db23d7ffffa2e8e6888311194c70ce73b3029..59aad912df75b687b4c2ebe7481dc2e9f5ca0a47 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -73,7 +73,7 @@ definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
 
 lemma injective_compose : ∀A,B,C,f,g.
 injective A B f → injective B C g → injective A C (λx.g (f x)).
-/3/; qed.
+/3/; qed-.
 
 (* extensional equality *)