aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/coqlib.mli')
-rw-r--r--interp/coqlib.mli6
1 files changed, 6 insertions, 0 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index dbe99e399..2c035cc34 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -19,6 +19,12 @@ open Pattern
(*s This module collects the global references, constructions and
patterns of the standard library used in ocaml files *)
+(*s Some utilities, the first argument is used for error messages.
+ Must be used lazyly. s*)
+
+val gen_reference : string->string list -> string -> global_reference
+val gen_constant : string->string list -> string -> constr
+
(*s Global references *)
(* Modules *)