diff options
Diffstat (limited to 'theories')
| -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. |