diff options
| -rw-r--r-- | theories/Init/Datatypes.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 4782194a39..092fce996f 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -246,7 +246,7 @@ 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. destruct c; intros H; constructor; inversion_clear H; auto. -Qed. +Defined. (** Identity *) |