diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-01 09:24:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-01 09:24:56 +0000 |
| commit | 13d449a37131f69ae9fce6c230974b926d579d28 (patch) | |
| tree | 8cdc88e1be6ed75fa483899870343c12417fca9b /theories/Init/Datatypes.v | |
| parent | 88770a6a1814eb57a161188cda1f4b9ae639c252 (diff) | |
Switched to "standardized" names for the properties of eq and
identity. Add notations for compatibility and support for
understanding these notations in the ml files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r-- | theories/Init/Datatypes.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index cb96f3f60..73e4924aa 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -114,8 +114,8 @@ Inductive Empty_set : Set :=. sole inhabitant is denoted [refl_identity A a] *) Inductive identity (A:Type) (a:A) : A -> Type := - refl_identity : identity (A:=A) a a. -Hint Resolve refl_identity: core. + identity_refl : identity a a. +Hint Resolve identity_refl: core. Implicit Arguments identity_ind [A]. Implicit Arguments identity_rec [A]. |