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 /interp | |
| parent | 27838d59f12fde650191c61f3d2168daa1ac2bd3 (diff) | |
| parent | 93dc998702e7c3ba13d3bc0250446dcad5fd027d (diff) | |
Merge PR #9529: Change Primitive message: "is registered" -> "is declared".
Reviewed-by: vbgl
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 3 | ||||
| -rw-r--r-- | interp/declare.mli | 1 |
2 files changed, 0 insertions, 4 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 175f9c66df..4371b15c82 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -430,9 +430,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 6f53d6872b..8f1e73c88c 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 *) -> |