Merge PR#678: [coqlib] Move `Coqlib` to `library/`.

3 files changed, 595 insertions, 0 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
new file mode 100644
index 0000000000..955ff4c089
--- /dev/null
+++ b/library/coqlib.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(*  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 Libnames
+open Globnames
+open Nametab
+
+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 dp = make_dir dir in
+  let sp = Libnames.make_path dp (Id.of_string s) in
+  try Nametab.global_of_path sp
+  with Not_found ->
+    (* Following bug 5066 we are more permissive with the handling
+       of not found errors here *)
+    user_err ~hdr:locstr
+      Pp.(str "cannot find " ++ Libnames.pr_path sp ++
+          str "; maybe library " ++ Libnames.pr_dirpath dp ++
+          str " has to be required first.")
+
+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 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_all qualid 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)
+
+(* 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 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"
+
+(** 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 : global_reference;
+  andb_prop : global_reference;
+  andb_true_intro : global_reference}
+
+let build_bool_type () =
+  { andb =  init_reference ["Datatypes"] "andb";
+    andb_prop =  init_reference ["Datatypes"] "andb_prop";
+    andb_true_intro =  init_reference ["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_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_reference ["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_reference ["Logic"] "False"
+
+(* The True proposition and its unique proof *)
+let coq_True   = lazy_init_reference ["Logic"] "True"
+let coq_I      = lazy_init_reference ["Logic"] "I"
+
+(* Connectives *)
+let coq_not = lazy_init_reference ["Logic"] "not"
+let coq_and = lazy_init_reference ["Logic"] "and"
+let coq_conj = lazy_init_reference ["Logic"] "conj"
+let coq_or = lazy_init_reference ["Logic"] "or"
+let coq_ex = lazy_init_reference ["Logic"] "ex"
+let coq_iff = lazy_init_reference ["Logic"] "iff"
+
+let coq_iff_left_proj  = lazy_init_reference ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_reference ["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 gen_reference = coq_reference
+
diff --git a/library/coqlib.mli b/library/coqlib.mli
new file mode 100644
index 0000000000..716d97c9d0
--- /dev/null
+++ b/library/coqlib.mli
@@ -0,0 +1,211 @@
+(************************************************************************)
+(*  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 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_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
+
+(** Identity  *)
+val id : constant
+val type_of_id : constant
+
+(** 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 : global_reference;
+  andb_prop : global_reference;
+  andb_true_intro : global_reference}
+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 : global_reference delayed
+
+(** {6 ... } *)
+(** Connectives 
+   The False proposition *)
+val build_coq_False : global_reference delayed
+
+(** The True proposition and its unique proof *)
+val build_coq_True : global_reference delayed
+val build_coq_I : global_reference delayed
+
+(** Negation *)
+val build_coq_not : global_reference delayed
+
+(** Conjunction *)
+val build_coq_and : global_reference delayed
+val build_coq_conj : global_reference delayed
+val build_coq_iff : global_reference delayed
+
+val build_coq_iff_left_proj : global_reference delayed
+val build_coq_iff_right_proj : global_reference delayed
+
+(** Disjunction *)
+val build_coq_or : global_reference delayed
+
+(** Existential quantifier *)
+val build_coq_ex : global_reference 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 gen_reference :  message -> string list -> string -> global_reference
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
diff --git a/library/library.mllib b/library/library.mllib
index df4f735034..6f433b77d1 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -16,3 +16,4 @@ Goptions
 Decls
 Heads
 Keys
+Coqlib