diff options
| author | Vincent Laporte | 2019-02-20 15:47:07 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-20 15:47:07 +0000 |
| commit | 924468eb648750bf2cbb6de0b1c8f7a2960f0bf5 (patch) | |
| tree | 65bfc4f704ee52bacc1abe39f3049b6a178fbe99 /vernac | |
| parent | 27838d59f12fde650191c61f3d2168daa1ac2bd3 (diff) | |
| parent | 93dc998702e7c3ba13d3bc0250446dcad5fd027d (diff) | |
Merge PR #9529: Change Primitive message: "is registered" -> "is declared".
Reviewed-by: vbgl
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 466757c6bd..4fb06e4e09 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") |