From c8bd5bc0f434d95f3244e44f7bc1731db3448050 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 24 Jan 2014 17:32:46 -0500
Subject: [Coercion]s use [Sortclass], not [Prop] (in docs)

Reported By: J. Ian Johnson
---
 theories/Init/Datatypes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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] *)
-- 
cgit v1.2.3