diff options
| author | Hugo Herbelin | 2015-12-14 15:04:52 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-01-14 14:36:10 +0100 |
| commit | 33617aa7b36f157f6314a83dde6ba45164ddd05b (patch) | |
| tree | fa412ff8488ac263b33e58392c5658226c3b0f82 /library | |
| parent | c7a7d55e0dc47a097bf0d0c8897bc490ce55577b (diff) | |
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).
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 *) |