diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2017-07-05 16:57:01 +0100 |
|---|---|---|
| committer | Tej Chajed <tchajed@mit.edu> | 2017-07-05 17:23:15 +0100 |
| commit | 466605a061dc2ef368b8c43c1f78f449b9db6045 (patch) | |
| tree | d7c05515c3fdc9e97ef650d4aeac03d8caaef73b /theories | |
| parent | 1111aeb445261af9e74770c0fe3bfd0ffd4930e2 (diff) | |
Fix typo in documentation for identity
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
Diffstat (limited to 'theories')
| -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 99937e8e0..22e10e2e4 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -336,7 +336,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined. (** [identity A a] is the family of datatypes on [A] whose sole non-empty member is the singleton datatype [identity A a a] whose - sole inhabitant is denoted [refl_identity A a] *) + sole inhabitant is denoted [identity_refl A a] *) Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. |