Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)

 There are currently two other clashs : Lexer and Errors, but for
 the moment these ones haven't impacted my experiments with extraction
 and compiler-libs, while this Matching issue had. And anyway the new
 name is more descriptive, in the spirit of the recent TacticMatching.

8 files changed, 28 insertions, 29 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 61e7dde181..3b99cc5b9e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -21,7 +21,6 @@ open Evd
 open Typing
 open Pattern
 open Patternops
-open Matching
 open Tacmach
 open Pfedit
 open Genredexpr
@@ -1115,10 +1114,12 @@ let conclPattern concl pat tac =
     match pat with
     | None -> Proofview.tclUNIT Id.Map.empty
     | Some pat ->
-	try Proofview.tclUNIT (matches pat concl)
-	with PatternMatchingFailure -> Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) in
-    constr_bindings >>= fun constr_bindings ->
-    Hook.get forward_interp_tactic constr_bindings tac
+	try Proofview.tclUNIT (ConstrMatching.matches pat concl)
+	with ConstrMatching.PatternMatchingFailure ->
+          Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
+  in
+  constr_bindings >>= fun constr_bindings ->
+  Hook.get forward_interp_tactic constr_bindings tac
 
 (***********************************************************)
 (** A debugging / verbosity framework for trivial and auto *)
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 4b1cd87150..7b47605119 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -23,7 +23,7 @@ open Declarations
 open Tactics
 open Tacticals
 open Auto
-open Matching
+open ConstrMatching
 open Hipattern
 open Tacmach
 open Coqlib
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1006fd2de7..2854d10194 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -25,7 +25,6 @@ open Typing
 open Retyping
 open Tacmach
 open Logic
-open Matching
 open Hipattern
 open Tacexpr
 open Tacticals
@@ -1383,7 +1382,7 @@ let decomp_tuple_term env c t =
       and cdr_code = applist (p2,[a;p;inner_code]) in
       let cdrtyp = beta_applist (p,[car]) in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
-    with PatternMatchingFailure ->
+    with ConstrMatching.PatternMatchingFailure ->
       []
     in
     [((ex,exty),inner_code)]::iterated_decomp
@@ -1458,7 +1457,7 @@ let try_rewrite tac gls =
   try
     tac gls
   with
-    | PatternMatchingFailure ->
+    | ConstrMatching.PatternMatchingFailure ->
 	errorlabstrm "try_rewrite" (str "Not a primitive equality here.")
     | e when catchable_exception e ->
 	errorlabstrm "try_rewrite"
@@ -1523,8 +1522,8 @@ let unfold_body x gl =
 
 let restrict_to_eq_and_identity eq = (* compatibility *)
   if not (eq_constr eq (constr_of_global glob_eq)) &&
-    not (eq_constr eq (constr_of_global glob_identity)) then
-    raise PatternMatchingFailure
+    not (eq_constr eq (constr_of_global glob_identity))
+  then raise ConstrMatching.PatternMatchingFailure
 
 exception FoundHyp of (Id.t * constr * bool)
 
@@ -1534,7 +1533,7 @@ let is_eq_x gl x (id,_,c) =
     let (_,lhs,rhs) = snd (find_eq_data_decompose gl c) in
     if (eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
     if (eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
-  with PatternMatchingFailure ->
+  with ConstrMatching.PatternMatchingFailure ->
     ()
 
 (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
@@ -1635,7 +1634,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
       if eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ ->
       match kind_of_term y with Var y -> y | _ -> failwith "caught"
-    with PatternMatchingFailure -> failwith "caught"
+    with ConstrMatching.PatternMatchingFailure -> failwith "caught"
   in
   let test p = try Some (test p) with Failure _ -> None in
   let hyps = Tacmach.New.pf_hyps_types gl in
@@ -1651,13 +1650,13 @@ let cond_eq_term_left c t gl =
   try
     let (_,x,_) = snd (find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true else failwith "not convertible"
-  with PatternMatchingFailure -> failwith "not an equality"
+  with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
     let (_,_,x) = snd (find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then false else failwith "not convertible"
-  with PatternMatchingFailure -> failwith "not an equality"
+  with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
@@ -1665,7 +1664,7 @@ let cond_eq_term c t gl =
     if pf_conv_x gl c x then true
     else if pf_conv_x gl c y then false
     else failwith "not convertible"
-  with PatternMatchingFailure -> failwith "not an equality"
+  with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t)
 let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t)
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 534b90491a..80720cfaf6 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -15,7 +15,7 @@ open Names
 open Term
 open Termops
 open Inductiveops
-open Matching
+open ConstrMatching
 open Coqlib
 open Declarations
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cd265843d3..0e802f8a9c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -9,7 +9,6 @@
 open Constrintern
 open Pattern
 open Patternops
-open Matching
 open Pp
 open Genredexpr
 open Glob_term
@@ -643,7 +642,7 @@ let interp_may_eval f ist env sigma = function
       (try
 	let (sigma,ic) = f ist env sigma c
 	and ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
-	sigma , subst_meta [special_meta,ic] ctxt
+	sigma , subst_meta [ConstrMatching.special_meta,ic] ctxt
       with
 	| Not_found ->
 	    user_err_loc (loc, "interp_may_eval",
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index e52a9011cf..85108f8ed2 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -19,7 +19,7 @@ open Tacexpr
     those of {!Matching.matching_result}), and a {!Term.constr}
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
-  subst : Matching.bound_ident_map * Pattern.extended_patvar_map ;
+  subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ;
   context : Term.constr Id.Map.t;
   terms : Term.constr Id.Map.t;
   lhs : 'a;
@@ -33,9 +33,9 @@ type 'a t = {
 (** Some of the functions of {!Matching} return the substitution with a
     [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
     substitution of the former type to the latter. *)
-let adjust : Matching.bound_ident_map * Pattern.patvar_map ->
-             Matching.bound_ident_map * Pattern.extended_patvar_map = fun (l, lc) ->
-  (l, Id.Map.map (fun c -> [], c) lc)
+let adjust : ConstrMatching.bound_ident_map * Pattern.patvar_map ->
+             ConstrMatching.bound_ident_map * Pattern.extended_patvar_map =
+  fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
 
 
 (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *)
@@ -240,19 +240,19 @@ module PatternMatching (E:StaticEnvironment) = struct
     | Term p ->
         begin 
           try
-            put_subst (Matching.extended_matches p term) <*>
+            put_subst (ConstrMatching.extended_matches p term) <*>
             return lhs
-          with Matching.PatternMatchingFailure -> fail
+          with ConstrMatching.PatternMatchingFailure -> fail
         end
     | Subterm (with_app_context,id_ctxt,p) ->
         (* spiwack: this branch is easier in direct style, would need to be
            changed if the implementation of the monad changes. *)
-        IStream.map begin fun { Matching.m_sub ; m_ctx } ->
+        IStream.map begin fun { ConstrMatching.m_sub ; m_ctx } ->
           let subst = adjust m_sub in
           let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
           let terms = empty_term_subst in
           { subst ; context ; terms ; lhs }
-        end (Matching.match_subterm_gen with_app_context p term)
+        end (ConstrMatching.match_subterm_gen with_app_context p term)
 
 
   (** [rule_match_term term rule] matches the term [term] with the
diff --git a/tactics/tacticMatching.mli b/tactics/tacticMatching.mli
index 1b440e195b..6889ea0e9b 100644
--- a/tactics/tacticMatching.mli
+++ b/tactics/tacticMatching.mli
@@ -17,7 +17,7 @@
     those of {!Matching.matching_result}), and a {!Term.constr}
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
-  subst : Matching.bound_ident_map * Pattern.extended_patvar_map ;
+  subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ;
   context : Term.constr Names.Id.Map.t;
   terms : Term.constr Names.Id.Map.t;
   lhs : 'a;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d1b096048d..a5f88c9291 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1416,7 +1416,7 @@ let my_find_eq_data_decompose gl t =
   with e when is_anomaly e
     (* Hack in case equality is not yet defined... one day, maybe,
        known equalities will be dynamically registered *)
-      -> raise Matching.PatternMatchingFailure
+      -> raise ConstrMatching.PatternMatchingFailure
 
 let intro_decomp_eq loc b l l' thin tac id gl =
   let c = mkVar id in