diff options
| -rw-r--r-- | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 14 |
2 files changed, 8 insertions, 8 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 9895bd30bc..d7e4b1ff63 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 a871c4081a..6025078673 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. |