diff options
| -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] *) |