diff options
| author | herbelin | 2006-08-28 13:45:32 +0000 |
|---|---|---|
| committer | herbelin | 2006-08-28 13:45:32 +0000 |
| commit | 0a921a91ec8d61d9abc3380949a6f06cf2a069ae (patch) | |
| tree | a996581378463d04e8a9cec5b98f36840f2f332d /theories/Init | |
| parent | a49d610f95a9d78d273cc34a82cc91ebfab2f22a (diff) | |
Passage à une définition de inhabited plus dans les 'standard mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 27fcb2f295..b505828d0e 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -312,4 +312,8 @@ intros A P; split. auto. Qed. +(** Being inhabited *) +Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A. + +Hint Resolve inhabits: core. |