diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-24 16:40:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-28 09:38:36 -0400 |
| commit | c6a05d73fc195cc7d5ffb62f2109617701d4791c (patch) | |
| tree | 60e2ff57def9525c920f96e299f95596845d6c66 /theories/Init | |
| parent | 37ff7235fe4d489a35458bb12abdf497480cf5c5 (diff) | |
Make theorems about ex equality Qed
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 8 |
1 files changed, 4 insertions, 4 deletions
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. |