[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

2 files changed, 45 insertions, 29 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 9539980f04..9105bdd54f 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -32,10 +32,6 @@ let find_reference locstr dir s =
     anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp)
 
 let coq_reference locstr dir s = find_reference locstr (coq::dir) s
-let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
-
-let gen_reference = coq_reference
-let gen_constant = coq_constant
 
 let has_suffix_in_dirs dirs ref =
   let dir = dirpath (path_of_global ref) in
@@ -68,7 +64,6 @@ let gen_reference_in_modules locstr dirs s =
 let gen_constant_in_modules locstr dirs s =
   Universes.constr_of_global (gen_reference_in_modules locstr dirs s)
 
-
 (* For tactics/commands requiring vernacular libraries *)
 
 let check_required_library d =
@@ -93,16 +88,16 @@ let check_required_library d =
 (* Specific Coq objects *)
 
 let init_reference dir s =
-  let d = "Init"::dir in
-  check_required_library (coq::d); gen_reference "Coqlib" d s
+  let d = coq::"Init"::dir in
+  check_required_library d; find_reference "Coqlib" d s
 
 let init_constant dir s =
-  let d = "Init"::dir in
-  check_required_library (coq::d); gen_constant "Coqlib" d s
+  let d = coq::"Init"::dir in
+  check_required_library d; Universes.constr_of_global @@ find_reference "Coqlib" d s
 
 let logic_reference dir s =
-  let d = "Logic"::dir in
-  check_required_library ("Coq"::d); gen_reference "Coqlib" d s
+  let d = coq::"Logic"::dir in
+  check_required_library d; find_reference "Coqlib" d s
 
 let arith_dir = [coq;"Arith"]
 let arith_modules = [arith_dir]
@@ -385,8 +380,8 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
-let coq_jmeq_ref     = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
-let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
+let coq_jmeq_ref     = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
+let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
 let coq_existS_ref  = lazy (anomaly (Pp.str "use coq_existT_ref"))
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_exist_ref  = lazy (init_reference ["Specif"] "exist")
@@ -397,3 +392,8 @@ let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
 let coq_or_ref     = lazy (init_reference ["Logic"] "or")
 let coq_iff_ref    = lazy (init_reference ["Logic"] "iff")
 
+(* Deprecated *)
+let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
+let gen_reference = coq_reference
+let gen_constant  = coq_constant
+
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 1facb47e1e..49802089d0 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"]
+