From c6a05d73fc195cc7d5ffb62f2109617701d4791c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 May 2017 16:40:31 -0400 Subject: Make theorems about ex equality Qed As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461 --- theories/Init/Logic.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4c0c18772..1cd2f4cde 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. -- cgit v1.2.3