diff options
| author | Maxime Dénès | 2017-07-20 13:14:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-20 13:14:38 +0200 |
| commit | 945d7bfa27b71137d86a4a46aeeced90d4b59303 (patch) | |
| tree | 438561788f99b0896eb905aeaf19b93e6687c3a5 /theories | |
| parent | 4d4ec6a095d01b6117ac3682d8a7882b1a2520e7 (diff) | |
| parent | d074e889b3cdfe8c292d3c52a4ed005789384fc0 (diff) | |
Merge branch 'v8.7'
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 99937e8e0f..22e10e2e43 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. |