doc and changes for coercion from prop/type

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 1c7c53f296..ee2205c981 100644
--- a/CHANGES
+++ b/CHANGES
@@ -77,6 +77,7 @@ Vernacular Commands
 - Using “Require” inside a section is deprecated.
 - An experimental command "Show Extraction" allows to extract the content
   of the current ongoing proof (grant wish #4129).
+- Coercion now accepts the type of its argument to be "Prop" or "Type".
 
 Universes