diff options
| author | letouzey | 2013-03-12 23:59:25 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-12 23:59:25 +0000 |
| commit | 1126ec7c771e18644c361fcdf1f8d59d6b7f73e7 (patch) | |
| tree | 8385285f7fecab4dc2eaec5ab26ae79582bb13a2 /interp | |
| parent | 66b098b04971f4bc08ce89afebdaec1772e3f73c (diff) | |
Hipattern : consider jmeq only when Logic.JMeq is loaded
Otherwise an Anomaly coming from Coqlib.find_reference is raised
and catched for the moment, but that will change soon.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16275 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 20 | ||||
| -rw-r--r-- | interp/coqlib.mli | 1 |
2 files changed, 11 insertions, 10 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 27d322a9c0..34ea7b607d 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -26,7 +26,8 @@ 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) + 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 coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s) @@ -63,15 +64,14 @@ let gen_constant_in_modules locstr dirs s = (* For tactics/commands requiring vernacular libraries *) let check_required_library d = - let d' = List.map Id.of_string d in - let dir = DirPath.make (List.rev d') in - let mp = (fst(Lib.current_prefix())) in - let current_dir = match mp with - | MPfile dp -> DirPath.equal dir dp - | _ -> false - in - if not (Library.library_is_loaded dir) then - if not current_dir then + let dir = make_dir d in + if Library.library_is_loaded dir then () + else + let in_current_dir = match Lib.current_prefix () 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 diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 37be549d6b..5fb206bece 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -56,6 +56,7 @@ val check_required_library : string list -> unit (** Modules *) val logic_module : DirPath.t val logic_type_module : DirPath.t +val jmeq_module : DirPath.t val datatypes_module_name : string list val logic_module_name : string list |