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.
---
 interp/declare.ml  | 3 ---
 interp/declare.mli | 1 -
 2 files changed, 4 deletions(-)

(limited to 'interp')

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 *) ->
-- 
cgit v1.2.3