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

3 files changed, 23 insertions, 18 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 27d322a9c..34ea7b607 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 37be549d6..5fb206bec 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
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 9adb237a9..fadc50661 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -352,9 +352,10 @@ let is_sigma_type t=op2bool (match_with_sigma_type t)
 
 let rec first_match matcher = function
   | [] -> raise PatternMatchingFailure
-  | (pat,build_set)::l ->
-      try (build_set (),matcher pat)
-      with PatternMatchingFailure -> first_match matcher l
+  | (pat,check,build_set)::l when check () ->
+      (try (build_set (),matcher pat)
+       with PatternMatchingFailure -> first_match matcher l)
+  | _::l -> first_match matcher l
 
 (*** Equality *)
 
@@ -375,10 +376,13 @@ let match_eq eqn eq_pat =
 	HeterogenousEq (t,x,t',x')
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms")
 
+let no_check () = true
+let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
+
 let equalities =
-  [coq_eq_pattern, build_coq_eq_data;
-   coq_jmeq_pattern, build_coq_jmeq_data;
-   coq_identity_pattern, build_coq_identity_data]
+  [coq_eq_pattern, no_check, build_coq_eq_data;
+   coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data;
+   coq_identity_pattern, no_check, build_coq_identity_data]
 
 let find_eq_data eqn = (* fails with PatternMatchingFailure *)
   first_match (match_eq eqn) equalities
@@ -439,8 +443,8 @@ let match_sigma ex ex_pat =
 
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   first_match (match_sigma ex)
-    [coq_existT_pattern, build_sigma_type;
-     coq_exist_pattern, build_sigma]
+    [coq_existT_pattern, no_check, build_sigma_type;
+     coq_exist_pattern, no_check, build_sigma]
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]