diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 21 | ||||
| -rw-r--r-- | interp/coqlib.mli | 3 |
2 files changed, 24 insertions, 0 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 113cb9d3f6..fa939d0aab 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -16,6 +16,9 @@ open Libnames open Pattern open Nametab +(************************************************************************) +(* Generic functions to find Coq objects *) + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let gen_reference locstr dir s = @@ -58,6 +61,24 @@ let gen_constant_in_modules locstr dirs s = " in module"^(if List.length dirs > 1 then "s " else " ")) ++ prlist_with_sep pr_coma pr_dirpath dirs) + +(* For tactics/commands requiring vernacular libraries *) + +let check_required_library d = + let d' = List.map id_of_string d in + let dir = make_dirpath (List.rev d') in + if not (Library.library_is_loaded dir) then +(* Loading silently ... + let m, prefix = list_sep_last d' in + read_library + (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) +*) +(* or failing ...*) + error ("Library "^(list_last d)^" has to be required first") + +(************************************************************************) +(* Specific Coq objects *) + let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 6741e1a0ac..64c83d7ebe 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -31,6 +31,9 @@ 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 + (*s Global references *) (* Modules *) |