From 33617aa7b36f157f6314a83dde6ba45164ddd05b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Dec 2015 15:04:52 +0100
Subject: Changing "P is assumed" to "P is declared".

The term "assumed" refers more to the type of the object than to the
name of the object. It is particularly misguiding when P:Prop since P
is assumed would suggest that a proof of P is assumed, and not that
the variable P itself is declared (see discussion with P. Castéran on
coqdev: "Chapter 4 of the Reference Manual", 8/10/2015).
---
 library/declare.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/declare.ml b/library/declare.ml
index c1697a434a..40858eeec6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -413,7 +413,10 @@ let definition_message id =
   Flags.if_verbose msg_info (pr_id id ++ str " is defined")
 
 let assumption_message id =
-  Flags.if_verbose msg_info (pr_id id ++ str " is assumed")
+  (* Changing "assumed" to "declared", "assuming" referring more to
+  the type of the object than to the name of the object (see
+  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
+  Flags.if_verbose msg_info (pr_id id ++ str " is declared")
 
 (** Global universe names, in a different summary *)
 
-- 
cgit v1.2.3