diff options
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]. |