From 93dc998702e7c3ba13d3bc0250446dcad5fd027d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 16:42:15 +0100
Subject: Change Primitive message: "is registered" -> "is declared".

"registered" sounds like it existed before the command.

This could use assumption_message which is currently the same, but I
don't think it has the right semantic.
---
 vernac/comAssumption.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 73d0be04df..12ab417a31 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Pp
 open CErrors
 open Util
 open Vars
@@ -54,7 +53,7 @@ match local with
   let () = assumption_message ident in
   let () =
     if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
-    Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++
+    Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
     strbrk " is not visible from current goals")
   in
   let r = VarRef ident in
@@ -203,4 +202,4 @@ let do_primitive id prim typopt =
               }
   in
   let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
-  register_message id.CAst.v
+  Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
-- 
cgit v1.2.3