aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/coqlib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/coqlib.mli')
-rw-r--r--library/coqlib.mli8
1 files changed, 2 insertions, 6 deletions
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 1e3c37a9e..cc22f1635 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -71,8 +71,8 @@ val jmeq_module_name : string list
val datatypes_module_name : string list
(** Identity *)
-val id : constant
-val type_of_id : constant
+val id : Constant.t
+val type_of_id : Constant.t
(** Natural numbers *)
val nat_path : full_path
@@ -205,7 +205,3 @@ 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"]