[coqlib] Deprecate redundant Coqlib functions.

We remove redundant functions `coq_constant`, `gen_reference`, and
`gen_constant`.

This is a first step towards a lazy binding of libraries references.
We have also chosen to untangle `constr` from `Coqlib`, as how to
instantiate the reference (in particular wrt universes) is a
client-side issue. (The client may want to provide an `evar_map` ?)

c.f. #186

1 files changed, 32 insertions, 16 deletions

diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 1facb47e1..49802089d 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -15,6 +15,25 @@ open Util
 (** This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
 
+(** The idea is to migrate to rebindable name-based approach, thus the
+    only function this FILE will provide will be:
+
+    [find_reference : string -> global_reference]
+
+    such that [find_reference "core.eq.type"] returns the proper [global_reference]
+
+    [bind_reference : string -> global_reference -> unit]
+
+    will bind a reference.
+
+    A feature based approach would be possible too.
+
+    Contrary to the old approach of raising an anomaly, we expect
+    tactics to gracefully fail in the absence of some primitive.
+
+    This is work in progress, see below.
+*)
+
 (** {6 ... } *)
 (** [find_reference caller_message [dir;subdir;...] s] returns a global
    reference to the name dir.subdir.(...).s; the corresponding module
@@ -25,31 +44,19 @@ open Util
 type message = string
 
 val find_reference : message -> string list -> string -> global_reference
-
-(** [coq_reference caller_message [dir;subdir;...] s] returns a
-   global reference to the name Coq.dir.subdir.(...).s *)
-
 val coq_reference : message -> string list -> string -> global_reference
 
-(** idem but return a term *)
-
-val coq_constant : message -> string list -> string -> constr
-
-(** Synonyms of [coq_constant] and [coq_reference] *)
-
-val gen_constant : message -> string list -> string -> constr
-val gen_reference :  message -> string list -> string -> global_reference
+(** For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
 
 (** Search in several modules (not prefixed by "Coq") *)
-val gen_constant_in_modules : string->string list list-> string -> constr
+val gen_constant_in_modules  : string->string list list-> string -> constr
 val gen_reference_in_modules : string->string list list-> string -> global_reference
+
 val arith_modules : string list list
 val zarith_base_modules : string list list
 val init_modules : string list list
 
-(** For tactics/commands requiring vernacular libraries *)
-val check_required_library : string list -> unit
-
 (** {6 Global references } *)
 
 (** Modules *)
@@ -196,3 +203,12 @@ val coq_sig_ref : global_reference lazy_t
 
 val coq_or_ref : global_reference lazy_t
 val coq_iff_ref : global_reference lazy_t
+
+(* Deprecated functions *)
+val coq_constant  : message -> string list -> string -> constr
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
+val gen_constant  : message -> string list -> string -> constr
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
+val gen_reference :  message -> string list -> string -> global_reference
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
+