Transparent

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

1 files changed, 6 insertions, 3 deletions

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.