diff options
| author | Jason Gross | 2014-01-24 17:32:46 -0500 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-24 23:53:00 +0100 |
| commit | c8bd5bc0f434d95f3244e44f7bc1731db3448050 (patch) | |
| tree | 622a653204fa1e29467a3cf53d01a2f56c815174 | |
| parent | 30986b6e7616e9c170b012bb00dff80603d84c76 (diff) | |
[Coercion]s use [Sortclass], not [Prop] (in docs)
Reported By: J. Ian Johnson
| -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 fc620f71d6..a956954544 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] *) |