Make theorems about ex equality Qed

As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4c0c187724..1cd2f4cde8 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -660,7 +660,7 @@ Section ex.
     destruct pq as [p q].
     destruct q; simpl in *.
     destruct p; reflexivity.
-  Defined.
+  Qed.
 
   Definition eq_ex {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1)
              (p : u1 = v1) (q : rew p in u2 = v2)
@@ -686,7 +686,7 @@ Section ex.
       end.
   Proof.
     destruct H, u; reflexivity.
-  Defined.
+  Qed.
 End ex.
 
 (** Equality for [ex2] *)
@@ -702,7 +702,7 @@ Section ex2.
     destruct pq as [p q r].
     destruct r, q, p; simpl in *.
     reflexivity.
-  Defined.
+  Qed.
 
   Definition eq_ex2 {A : Type} {P Q : A -> Prop}
              (u1 v1 : A)
@@ -740,5 +740,5 @@ Section ex2.
       end.
   Proof.
     destruct H, u; reflexivity.
-  Defined.
+  Qed.
 End ex2.