[coqlib] Move `Coqlib` to `library/`.

We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.

By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.

Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.

The main changes are:

- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
  have different needs with regards to universes/evar_maps, so we
  force them to call the (not very safe) `Universes.constr_of_global`
  explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
  `pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
  anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
  illustrates the danger of duplication in the code base; the solution
  chosen there was to transform the not-found anomaly into an error
  message, however the general policy was far from clear. The long
  term solution is indeed make `find_reference` emit `Not_found` and
  let the client handle the error maybe non-fatally. (so they can test
  for constants.

3 files changed, 0 insertions, 614 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
deleted file mode 100644
index 9105bdd54..000000000
--- a/interp/coqlib.ml
+++ /dev/null
@@ -1,399 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open CErrors
-open Util
-open Pp
-open Names
-open Term
-open Libnames
-open Globnames
-open Nametab
-open Smartlocate
-
-let coq = Nameops.coq_string (* "Coq" *)
-
-(************************************************************************)
-(* Generic functions to find Coq objects *)
-
-type message = string
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-
-let find_reference locstr dir s =
-  let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
-  try global_of_extended_global (Nametab.extended_global_of_path sp)
-  with Not_found ->
-    anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp)
-
-let coq_reference locstr dir s = find_reference locstr (coq::dir) s
-
-let has_suffix_in_dirs dirs ref =
-  let dir = dirpath (path_of_global ref) in
-  List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
-
-let global_of_extended q =
-  try Some (global_of_extended_global q) with Not_found -> None
-
-let gen_reference_in_modules locstr dirs s =
-  let dirs = List.map make_dir dirs in
-  let qualid = qualid_of_string s in
-  let all = Nametab.locate_extended_all qualid in
-  let all = List.map_filter global_of_extended all in
-  let all = List.sort_uniquize RefOrdered_env.compare all in
-  let these = List.filter (has_suffix_in_dirs dirs) all in
-  match these with
-    | [x] -> x
-    | [] ->
-	anomaly ~label:locstr (str "cannot find " ++ str s ++
-	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
-	prlist_with_sep pr_comma pr_dirpath dirs)
-    | l ->
-      anomaly ~label:locstr
-	(str "ambiguous name " ++ str s ++ str " can represent " ++
-	   prlist_with_sep pr_comma
-	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
-	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
-	   prlist_with_sep pr_comma pr_dirpath dirs)
-
-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 =
-  let dir = make_dir d in
-  if Library.library_is_loaded dir then ()
-  else
-    let in_current_dir = match Lib.current_mp () with
-      | MPfile dp -> DirPath.equal dir dp
-      | _ -> false
-    in
-    if not in_current_dir then
-(* Loading silently ...
-    let m, prefix = List.sep_last d' in
-    read_library
-     (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
-*)
-(* or failing ...*)
-      user_err ~hdr:"Coqlib.check_required_library"
-        (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
-
-(************************************************************************)
-(* Specific Coq objects *)
-
-let init_reference dir s =
-  let d = coq::"Init"::dir in
-  check_required_library d; find_reference "Coqlib" d s
-
-let init_constant dir 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 = coq::"Logic"::dir in
-  check_required_library d; find_reference "Coqlib" d s
-
-let arith_dir = [coq;"Arith"]
-let arith_modules = [arith_dir]
-
-let numbers_dir = [coq;"Numbers"]
-let parith_dir = [coq;"PArith"]
-let narith_dir = [coq;"NArith"]
-let zarith_dir = [coq;"ZArith"]
-
-let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
-
-let init_dir = [coq;"Init"]
-let init_modules = [
-  init_dir@["Datatypes"];
-  init_dir@["Logic"];
-  init_dir@["Specif"];
-  init_dir@["Logic_Type"];
-  init_dir@["Nat"];
-  init_dir@["Peano"];
-  init_dir@["Wf"]
-]
-
-let prelude_module_name = init_dir@["Prelude"]
-let prelude_module = make_dir prelude_module_name
-
-let logic_module_name = init_dir@["Logic"]
-let logic_module = make_dir logic_module_name
-
-let logic_type_module_name = init_dir@["Logic_Type"]
-let logic_type_module = make_dir logic_type_module_name
-
-let datatypes_module_name = init_dir@["Datatypes"]
-let datatypes_module = make_dir datatypes_module_name
-
-let jmeq_module_name = [coq;"Logic";"JMeq"]
-let jmeq_module = make_dir jmeq_module_name
-
-(* TODO: temporary hack. Works only if the module isn't an alias *)
-let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
-let make_con dir id = Globnames.encode_con dir (Id.of_string id)
-
-(** Identity *)
-
-let id = make_con datatypes_module "idProp"
-let type_of_id = make_con datatypes_module "IDProp"
-
-let _ = Termops.set_impossible_default_clause 
-  (fun () -> 
-    let c, ctx = Universes.fresh_global_instance (Global.env()) (ConstRef id) in
-    let (_, u) = destConst c in
-      (c,mkConstU (type_of_id,u)), ctx)
-
-(** Natural numbers *)
-let nat_kn = make_ind datatypes_module "nat"
-let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
-
-let glob_nat = IndRef (nat_kn,0)
-
-let path_of_O = ((nat_kn,0),1)
-let path_of_S = ((nat_kn,0),2)
-let glob_O = ConstructRef path_of_O
-let glob_S = ConstructRef path_of_S
-
-(** Booleans *)
-let bool_kn = make_ind datatypes_module "bool"
-
-let glob_bool = IndRef (bool_kn,0)
-
-let path_of_true = ((bool_kn,0),1)
-let path_of_false = ((bool_kn,0),2)
-let glob_true  = ConstructRef path_of_true
-let glob_false  = ConstructRef path_of_false
-
-(** Equality *)
-let eq_kn = make_ind logic_module "eq"
-let glob_eq = IndRef (eq_kn,0)
-
-let identity_kn = make_ind datatypes_module "identity"
-let glob_identity = IndRef (identity_kn,0)
-
-let jmeq_kn = make_ind jmeq_module "JMeq"
-let glob_jmeq = IndRef (jmeq_kn,0)
-
-type coq_sigma_data = {
-  proj1 : global_reference;
-  proj2 : global_reference;
-  elim  : global_reference;
-  intro : global_reference;
-  typ   : global_reference }
-
-type coq_bool_data  = {
-  andb : constr;
-  andb_prop : constr;
-  andb_true_intro : constr}
-
-let build_bool_type () =
-  { andb =  init_constant ["Datatypes"] "andb";
-    andb_prop =  init_constant ["Datatypes"] "andb_prop";
-    andb_true_intro =  init_constant ["Datatypes"] "andb_true_intro" }
-
-let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
-
-let build_sigma_type () =
-  { proj1 = init_reference ["Specif"] "projT1";
-    proj2 = init_reference ["Specif"] "projT2";
-    elim = init_reference ["Specif"] "sigT_rect";
-    intro = init_reference ["Specif"] "existT";
-    typ = init_reference ["Specif"] "sigT" }
-
-let build_sigma () =
-  { proj1 = init_reference ["Specif"] "proj1_sig";
-    proj2 = init_reference ["Specif"] "proj2_sig";
-    elim = init_reference ["Specif"] "sig_rect";
-    intro = init_reference ["Specif"] "exist";
-    typ = init_reference ["Specif"] "sig" }
-
-
-let build_prod () =
-  { proj1 = init_reference ["Datatypes"] "fst";
-    proj2 = init_reference ["Datatypes"] "snd";
-    elim = init_reference ["Datatypes"] "prod_rec";
-    intro = init_reference ["Datatypes"] "pair";
-    typ = init_reference ["Datatypes"] "prod" }
-
-(* Equalities *)
-type coq_eq_data = {
-  eq   : global_reference;
-  ind  : global_reference;
-  refl : global_reference;
-  sym  : global_reference;
-  trans: global_reference;
-  congr: global_reference }
-
-(* Data needed for discriminate and injection *)
-type coq_inversion_data = {
-  inv_eq   : global_reference; (* : forall params, t -> Prop *)
-  inv_ind  : global_reference; (* : forall params P y, eq params y -> P y *)
-  inv_congr: global_reference  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
-}
-
-let lazy_init_reference dir id = lazy (init_reference dir id)
-let lazy_init_constant dir id = lazy (init_constant dir id)
-let lazy_logic_reference dir id = lazy (logic_reference dir id)
-
-(* Leibniz equality on Type *)
-
-let coq_eq_eq = lazy_init_reference ["Logic"] "eq"
-let coq_eq_refl = lazy_init_reference ["Logic"] "eq_refl"
-let coq_eq_ind = lazy_init_reference ["Logic"] "eq_ind"
-let coq_eq_congr = lazy_init_reference ["Logic"] "f_equal"
-let coq_eq_sym  = lazy_init_reference ["Logic"] "eq_sym"
-let coq_eq_trans  = lazy_init_reference ["Logic"] "eq_trans"
-let coq_f_equal2 = lazy_init_reference ["Logic"] "f_equal2"
-let coq_eq_congr_canonical =
-  lazy_init_reference ["Logic"] "f_equal_canonical_form"
-
-let build_coq_eq_data () =
-  let _ = check_required_library logic_module_name in {
-  eq = Lazy.force coq_eq_eq;
-  ind = Lazy.force coq_eq_ind;
-  refl = Lazy.force coq_eq_refl;
-  sym = Lazy.force coq_eq_sym;
-  trans = Lazy.force coq_eq_trans;
-  congr = Lazy.force coq_eq_congr }
-
-let build_coq_eq () = Lazy.force coq_eq_eq
-let build_coq_eq_refl () = Lazy.force coq_eq_refl
-let build_coq_eq_sym () = Lazy.force coq_eq_sym
-let build_coq_f_equal2 () = Lazy.force coq_f_equal2
-
-let build_coq_inversion_eq_data () =
-  let _ = check_required_library logic_module_name in {
-  inv_eq = Lazy.force coq_eq_eq;
-  inv_ind = Lazy.force coq_eq_ind;
-  inv_congr = Lazy.force coq_eq_congr_canonical }
-
-(* Heterogenous equality on Type *)
-
-let coq_jmeq_eq = lazy_logic_reference ["JMeq"] "JMeq"
-let coq_jmeq_hom = lazy_logic_reference ["JMeq"] "JMeq_hom"
-let coq_jmeq_refl = lazy_logic_reference ["JMeq"] "JMeq_refl"
-let coq_jmeq_ind = lazy_logic_reference ["JMeq"] "JMeq_ind"
-let coq_jmeq_sym  = lazy_logic_reference ["JMeq"] "JMeq_sym"
-let coq_jmeq_congr  = lazy_logic_reference ["JMeq"] "JMeq_congr"
-let coq_jmeq_trans  = lazy_logic_reference ["JMeq"] "JMeq_trans"
-let coq_jmeq_congr_canonical =
-  lazy_logic_reference ["JMeq"] "JMeq_congr_canonical_form"
-
-let build_coq_jmeq_data () =
-  let _ = check_required_library jmeq_module_name in {
-  eq = Lazy.force coq_jmeq_eq;
-  ind = Lazy.force coq_jmeq_ind;
-  refl = Lazy.force coq_jmeq_refl;
-  sym = Lazy.force coq_jmeq_sym;
-  trans = Lazy.force coq_jmeq_trans;
-  congr = Lazy.force coq_jmeq_congr }
-
-let build_coq_inversion_jmeq_data () =
-  let _ = check_required_library logic_module_name in {
-  inv_eq = Lazy.force coq_jmeq_hom;
-  inv_ind = Lazy.force coq_jmeq_ind;
-  inv_congr = Lazy.force coq_jmeq_congr_canonical }
-
-(* Specif *)
-let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
-
-let build_coq_sumbool () = Lazy.force coq_sumbool
-
-(* Equality on Type as a Type *)
-let coq_identity_eq = lazy_init_reference ["Datatypes"] "identity"
-let coq_identity_refl = lazy_init_reference ["Datatypes"] "identity_refl"
-let coq_identity_ind = lazy_init_reference ["Datatypes"] "identity_ind"
-let coq_identity_congr = lazy_init_reference ["Logic_Type"] "identity_congr"
-let coq_identity_sym = lazy_init_reference ["Logic_Type"] "identity_sym"
-let coq_identity_trans = lazy_init_reference ["Logic_Type"] "identity_trans"
-let coq_identity_congr_canonical = lazy_init_reference ["Logic_Type"] "identity_congr_canonical_form"
-
-let build_coq_identity_data () =
-  let _ = check_required_library datatypes_module_name in {
-  eq = Lazy.force coq_identity_eq;
-  ind = Lazy.force coq_identity_ind;
-  refl = Lazy.force coq_identity_refl;
-  sym = Lazy.force coq_identity_sym;
-  trans = Lazy.force coq_identity_trans;
-  congr = Lazy.force coq_identity_congr }
-
-let build_coq_inversion_identity_data () =
-  let _ = check_required_library datatypes_module_name in
-  let _ = check_required_library logic_type_module_name in {
-  inv_eq = Lazy.force coq_identity_eq;
-  inv_ind = Lazy.force coq_identity_ind;
-  inv_congr = Lazy.force coq_identity_congr_canonical }
-
-(* Equality to true *)
-let coq_eq_true_eq = lazy_init_reference ["Datatypes"] "eq_true"
-let coq_eq_true_ind = lazy_init_reference ["Datatypes"] "eq_true_ind"
-let coq_eq_true_congr = lazy_init_reference ["Logic"] "eq_true_congr"
-
-let build_coq_inversion_eq_true_data () =
-  let _ = check_required_library datatypes_module_name in
-  let _ = check_required_library logic_module_name in {
-  inv_eq = Lazy.force coq_eq_true_eq;
-  inv_ind = Lazy.force coq_eq_true_ind;
-  inv_congr = Lazy.force coq_eq_true_congr }
-
-(* The False proposition *)
-let coq_False  = lazy_init_constant ["Logic"] "False"
-
-(* The True proposition and its unique proof *)
-let coq_True   = lazy_init_constant ["Logic"] "True"
-let coq_I      = lazy_init_constant ["Logic"] "I"
-
-(* Connectives *)
-let coq_not = lazy_init_constant ["Logic"] "not"
-let coq_and = lazy_init_constant ["Logic"] "and"
-let coq_conj = lazy_init_constant ["Logic"] "conj"
-let coq_or = lazy_init_constant ["Logic"] "or"
-let coq_ex = lazy_init_constant ["Logic"] "ex"
-let coq_iff = lazy_init_constant ["Logic"] "iff"
-
-let coq_iff_left_proj  = lazy_init_constant ["Logic"] "proj1"
-let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2"
-
-(* Runtime part *)
-let build_coq_True ()  = Lazy.force coq_True
-let build_coq_I ()     = Lazy.force coq_I
-
-let build_coq_False () = Lazy.force coq_False
-let build_coq_not ()   = Lazy.force coq_not
-let build_coq_and ()   = Lazy.force coq_and
-let build_coq_conj ()  = Lazy.force coq_conj
-let build_coq_or ()    = Lazy.force coq_or
-let build_coq_ex ()    = Lazy.force coq_ex
-let build_coq_iff ()   = Lazy.force coq_iff
-
-let build_coq_iff_left_proj ()  = Lazy.force coq_iff_left_proj
-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 (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")
-let coq_not_ref     = lazy (init_reference ["Logic"] "not")
-let coq_False_ref   = lazy (init_reference ["Logic"] "False")
-let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
-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
deleted file mode 100644
index 49802089d..000000000
--- a/interp/coqlib.mli
+++ /dev/null
@@ -1,214 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Libnames
-open Globnames
-open Term
-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
-   must have been required or in the process of being compiled so that
-   it must be used lazily; it raises an anomaly with the given message
-   if not found *)
-
-type message = string
-
-val find_reference : message -> string list -> string -> global_reference
-val coq_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_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
-
-(** {6 Global references } *)
-
-(** Modules *)
-val prelude_module : DirPath.t
-
-val logic_module : DirPath.t
-val logic_module_name : string list
-
-val logic_type_module : DirPath.t
-
-val jmeq_module : DirPath.t
-val jmeq_module_name : string list
-
-val datatypes_module_name : string list
-
-(** Natural numbers *)
-val nat_path : full_path
-val glob_nat : global_reference
-val path_of_O : constructor
-val path_of_S : constructor
-val glob_O : global_reference
-val glob_S : global_reference
-
-(** Booleans *)
-val glob_bool : global_reference
-val path_of_true : constructor
-val path_of_false : constructor
-val glob_true : global_reference
-val glob_false : global_reference
-
-
-(** Equality *)
-val glob_eq : global_reference
-val glob_identity : global_reference
-val glob_jmeq : global_reference
-
-(** {6 ... } *)
-(** Constructions and patterns related to Coq initial state are unknown
-   at compile time. Therefore, we can only provide methods to build
-   them at runtime. This is the purpose of the [constr delayed] and
-   [constr_pattern delayed] types. Objects of this time needs to be
-   forced with [delayed_force] to get the actual constr or pattern 
-   at runtime. *)
-
-type coq_bool_data = {
-  andb : constr;
-  andb_prop : constr;
-  andb_true_intro : constr}
-val build_bool_type : coq_bool_data delayed
-
-(** {6 For Equality tactics } *)
-type coq_sigma_data = {
-  proj1 : global_reference;
-  proj2 : global_reference;
-  elim  : global_reference;
-  intro : global_reference;
-  typ   : global_reference }
-
-val build_sigma_set : coq_sigma_data delayed
-val build_sigma_type : coq_sigma_data delayed
-val build_sigma : coq_sigma_data delayed
-
-(* val build_sigma_type_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
-(* val build_sigma_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
-(* val build_prod_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *)
-(* val build_coq_eq_data_in : Environ.env -> coq_eq_data Univ.in_universe_context_set *)
-
-(** Non-dependent pairs in Set from Datatypes *)
-val build_prod : coq_sigma_data delayed
-
-type coq_eq_data = {
-  eq   : global_reference;
-  ind  : global_reference;
-  refl : global_reference;
-  sym  : global_reference;
-  trans: global_reference;
-  congr: global_reference }
-
-val build_coq_eq_data : coq_eq_data delayed
-
-val build_coq_identity_data : coq_eq_data delayed
-val build_coq_jmeq_data : coq_eq_data delayed
-
-val build_coq_eq       : global_reference delayed (** = [(build_coq_eq_data()).eq] *)
-val build_coq_eq_refl  : global_reference delayed (** = [(build_coq_eq_data()).refl] *)
-val build_coq_eq_sym   : global_reference delayed (** = [(build_coq_eq_data()).sym] *)
-val build_coq_f_equal2 : global_reference delayed
-
-(** Data needed for discriminate and injection *)
-
-type coq_inversion_data = {
-  inv_eq   : global_reference; (** : forall params, args -> Prop *)
-  inv_ind  : global_reference; (** : forall params P (H : P params) args, eq params args 
-			 ->  P args *)
-  inv_congr: global_reference  (** : forall params B (f:t->B) args, eq params args -> 
-			 f params = f args *)
-}
-
-val build_coq_inversion_eq_data : coq_inversion_data delayed
-val build_coq_inversion_identity_data : coq_inversion_data delayed
-val build_coq_inversion_jmeq_data : coq_inversion_data delayed
-val build_coq_inversion_eq_true_data : coq_inversion_data delayed
-
-(** Specif *)
-val build_coq_sumbool : constr delayed
-
-(** {6 ... } *)
-(** Connectives 
-   The False proposition *)
-val build_coq_False : constr delayed
-
-(** The True proposition and its unique proof *)
-val build_coq_True : constr delayed
-val build_coq_I : constr delayed
-
-(** Negation *)
-val build_coq_not : constr delayed
-
-(** Conjunction *)
-val build_coq_and : constr delayed
-val build_coq_conj : constr delayed
-val build_coq_iff : constr delayed
-
-val build_coq_iff_left_proj : constr delayed
-val build_coq_iff_right_proj : constr delayed
-
-(** Disjunction *)
-val build_coq_or : constr delayed
-
-(** Existential quantifier *)
-val build_coq_ex : constr delayed
-
-val coq_eq_ref : global_reference lazy_t
-val coq_identity_ref : global_reference lazy_t
-val coq_jmeq_ref : global_reference lazy_t
-val coq_eq_true_ref : global_reference lazy_t
-val coq_existS_ref : global_reference lazy_t
-val coq_existT_ref : global_reference lazy_t
-val coq_exist_ref : global_reference lazy_t
-val coq_not_ref : global_reference lazy_t
-val coq_False_ref : global_reference lazy_t
-val coq_sumbool_ref : global_reference lazy_t
-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"]
-
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 607af82a0..6d290a325 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -14,6 +14,5 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Coqlib
 Discharge
 Declare