diff options
| author | Gaëtan Gilbert | 2019-02-08 16:42:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 16:52:50 +0100 |
| commit | 93dc998702e7c3ba13d3bc0250446dcad5fd027d (patch) | |
| tree | ea0a3413f15dbd1b3867c913791d3cfbbe59f54b | |
| parent | 8c1c7601674f150a969223c67f3e963141b07b4f (diff) | |
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.
| -rw-r--r-- | interp/declare.ml | 3 | ||||
| -rw-r--r-- | interp/declare.mli | 1 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 5 |
3 files changed, 2 insertions, 7 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index ea6ed8321d..6778fa1e7a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -442,9 +442,6 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -let register_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered") - (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = diff --git a/interp/declare.mli b/interp/declare.mli index 669657af6f..468e056909 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -74,7 +74,6 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool val definition_message : Id.t -> unit val assumption_message : Id.t -> unit -val register_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> 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") |