diff options
author | Jason Gross <jgross@mit.edu> | 2014-01-24 17:32:46 -0500 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-24 23:53:00 +0100 |
commit | c8bd5bc0f434d95f3244e44f7bc1731db3448050 (patch) | |
tree | 622a653204fa1e29467a3cf53d01a2f56c815174 /theories/Init/Datatypes.v | |
parent | 30986b6e7616e9c170b012bb00dff80603d84c76 (diff) |
[Coercion]s use [Sortclass], not [Prop] (in docs)
Reported By: J. Ian Johnson
Diffstat (limited to 'theories/Init/Datatypes.v')
-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 fc620f71d..a95695454 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -87,7 +87,7 @@ Hint Constructors eq_true : eq_true. Definition is_true b := b = true. (** [is_true] can be activated as a coercion by - (Local) Coercion is_true : bool >-> Prop. + ([Local]) [Coercion is_true : bool >-> Sortclass]. *) (** Additional rewriting lemmas about [eq_true] *) |