Transparent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 9 insertions, 6 deletions

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index d847a060d..694351b67 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -15,17 +15,17 @@ Proof.
 NewInduction n.
 Auto.
 Left; Exists n; Auto.
-Qed.
+Defined.
 
 Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}.
 Proof.
 NewInduction n; NewInduction m; Auto.
 Elim (IHn m); Auto.
-Qed.
+Defined.
 
 Hints Resolve O_or_S eq_nat_dec : arith.
 
 Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
 Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
-Qed.
+Defined.
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 14f331930..645f4b0d7 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -139,17 +139,20 @@ Section Logic_lemmas.
     Theorem sym_eq : (eq ? x y) -> (eq ? y x).
       Proof.
      Induction 1; Trivial.
-    Qed.
+    Defined.
+    Opaque sym_eq.
 
     Theorem trans_eq : (eq ? x y) -> (eq ? y z) -> (eq ? x z).
     Proof.
      Induction 2; Trivial.
-    Qed.
+    Defined.
+    Opaque trans_eq.
 
     Theorem f_equal : (eq ? x y) -> (eq ? (f x) (f y)).
     Proof.
      Induction 1; Trivial.
-    Qed.
+    Defined.
+    Opaque f_equal.
 
     Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)).
     Proof.