Init: some results in Type should rather be Defined than Qed

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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9895bd30b..d7e4b1ff6 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -271,7 +271,7 @@ Hint Unfold CompSpec CompSpecT.
 
 Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
  CompSpec eq lt x y c -> CompSpecT eq lt x y c.
-Proof. intros. apply CompareSpec2Type; assumption. Qed.
+Proof. intros. apply CompareSpec2Type; assumption. Defined.
 
 (** Identity *)
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index a871c4081..602507867 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -153,16 +153,16 @@ Section Choice_lemmas.
   Proof.
    intro H.
    exists (fun z => proj1_sig (H z)).
-   intro z; destruct (H z); trivial.
-  Qed.
+   intro z; destruct (H z); assumption.
+  Defined.
 
   Lemma Choice2 :
    (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}.
   Proof.
     intro H.
     exists (fun z => projT1 (H z)).
-    intro z; destruct (H z); trivial.
-  Qed.
+    intro z; destruct (H z); assumption.
+  Defined.
 
   Lemma bool_choice :
    (forall x:S, {R1 x} + {R2 x}) ->
@@ -171,7 +171,7 @@ Section Choice_lemmas.
     intro H.
     exists (fun z:S => if H z then true else false).
     intro z; destruct (H z); auto.
-  Qed.
+  Defined.
 
 End Choice_lemmas.
 
@@ -189,7 +189,7 @@ Section Dependent_choice_lemmas.
     exists f.
     split. reflexivity.
     induction n; simpl; apply proj2_sig.
-  Qed.
+  Defined.
 
 End Dependent_choice_lemmas.
 
@@ -216,7 +216,7 @@ Proof.
   intros A C h1 h2.
   apply False_rec.
   apply (h2 h1).
-Qed.
+Defined.
 
 Hint Resolve left right inleft inright: core v62.
 Hint Resolve exist exist2 existT existT2: core.