Avoiding introducing yet another convention in naming files.

8 files changed, 26 insertions, 26 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ef6c38bf6c..fc4a459dec 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -129,8 +129,8 @@ let conclPattern concl pat tac =
     | None -> Proofview.tclUNIT Id.Map.empty
     | Some pat ->
 	try
-	  Proofview.tclUNIT (ConstrMatching.matches env sigma pat concl)
-	with ConstrMatching.PatternMatchingFailure ->
+	  Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
+	with Constr_matching.PatternMatchingFailure ->
           Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
   in
    Proofview.Goal.enter (fun gl ->
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index df8a018bb8..70490722e6 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -23,7 +23,7 @@ open Declarations
 open Tactics
 open Tacticals.New
 open Auto
-open ConstrMatching
+open Constr_matching
 open Hipattern
 open Tacmach.New
 open Coqlib
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9740f6c1f8..02d163acae 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1437,7 +1437,7 @@ let decomp_tuple_term env c t =
       and cdr_code = applist (mkConstU (destConstRef p2,i),[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 ConstrMatching.PatternMatchingFailure ->
+    with Constr_matching.PatternMatchingFailure ->
       []
     in [((ex,exty),inner_code)]::iterated_decomp
   in decomprec (mkRel 1) c t
@@ -1508,7 +1508,7 @@ let cutSubstInHyp l2r eqn id =
 
 let try_rewrite tac =
   Proofview.tclORELSE tac begin function (e, info) -> match e with
-    | ConstrMatching.PatternMatchingFailure ->
+    | Constr_matching.PatternMatchingFailure ->
 	tclZEROMSG (str "Not a primitive equality here.")
     | e when catchable_exception e ->
 	tclZEROMSG
@@ -1581,7 +1581,7 @@ let unfold_body x =
 let restrict_to_eq_and_identity eq = (* compatibility *)
   if not (is_global glob_eq eq) &&
     not (is_global glob_identity eq) 
-  then raise ConstrMatching.PatternMatchingFailure
+  then raise Constr_matching.PatternMatchingFailure
 
 exception FoundHyp of (Id.t * constr * bool)
 
@@ -1592,7 +1592,7 @@ let is_eq_x gl x (id,_,c) =
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
     if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
     if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
-  with ConstrMatching.PatternMatchingFailure ->
+  with Constr_matching.PatternMatchingFailure ->
     ()
 
 (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
@@ -1684,7 +1684,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
       if Term.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 ConstrMatching.PatternMatchingFailure -> failwith "caught"
+    with Constr_matching.PatternMatchingFailure -> failwith "caught"
   in
   let test p = try Some (test p) with Failure _ -> None in
   let hyps = pf_hyps_types gl in
@@ -1700,13 +1700,13 @@ let cond_eq_term_left c t gl =
   try
     let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true else failwith "not convertible"
-  with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
+  with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
     let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then false else failwith "not convertible"
-  with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
+  with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
@@ -1714,7 +1714,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 ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
+  with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let rewrite_assumption_cond cond_eq_term cl =
   let rec arec hyps gl = match hyps with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 89f6fbc747..a3862de582 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -729,7 +729,7 @@ let interp_may_eval f ist env sigma = function
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let evdref = ref sigma in
-	let c = subst_meta [ConstrMatching.special_meta,ic] ctxt in
+	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
 	let c = Typing.solve_evars env evdref c in
 	!evdref , c
       with
@@ -1528,8 +1528,8 @@ and interp_letin ist llc u =
   fold ist.lfun llc
 
 (** [interp_match_success lz ist succ] interprets a single matching success
-    (of type {!TacticMatching.t}). *)
-and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } =
+    (of type {!Tactic_matching.t}). *)
+and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   let (>>=) = Ftactic.bind in
   let lctxt = Id.Map.map interp_context context in
   let hyp_subst = Id.Map.map Value.of_constr terms in
@@ -1590,7 +1590,7 @@ and interp_match ist lz constr lmr =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
-    interp_match_successes lz ist (TacticMatching.match_term env sigma constr ilr)
+    interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr)
   end
 
 (* Interprets the Match Context expressions *)
@@ -1602,7 +1602,7 @@ and interp_match_goal ist lz lr lmr =
       let hyps = if lr then List.rev hyps else hyps in
       let concl = Proofview.Goal.concl gl in
       let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
-      interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr)
+      interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr)
     end
 
 (* Interprets extended tactic generic arguments *)
diff --git a/tactics/tacticMatching.ml b/tactics/tactic_matching.ml
index 52fa2e4a2d..f4b13bba85 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tactic_matching.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 : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ;
+  subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
   context : Term.constr Id.Map.t;
   terms : Term.constr Id.Map.t;
   lhs : 'a;
@@ -33,8 +33,8 @@ 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 : ConstrMatching.bound_ident_map * Pattern.patvar_map ->
-             ConstrMatching.bound_ident_map * Pattern.extended_patvar_map =
+let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map ->
+             Constr_matching.bound_ident_map * Pattern.extended_patvar_map =
   fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
 
 
@@ -230,16 +230,16 @@ module PatternMatching (E:StaticEnvironment) = struct
     | Term p ->
         begin 
           try
-            put_subst (ConstrMatching.extended_matches E.env E.sigma p term) <*>
+            put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
             return lhs
-          with ConstrMatching.PatternMatchingFailure -> fail
+          with Constr_matching.PatternMatchingFailure -> fail
         end
     | Subterm (with_app_context,id_ctxt,p) ->
 
       let rec map s (e, info) =
         { stream = fun k ctx -> match IStream.peek s with
           | IStream.Nil -> Proofview.tclZERO ~info e
-          | IStream.Cons ({ ConstrMatching.m_sub ; m_ctx }, s) ->
+          | IStream.Cons ({ Constr_matching.m_sub ; m_ctx }, s) ->
             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
@@ -249,7 +249,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
+      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the
diff --git a/tactics/tacticMatching.mli b/tactics/tactic_matching.mli
index 989f07d671..abeb47c3b9 100644
--- a/tactics/tacticMatching.mli
+++ b/tactics/tactic_matching.mli
@@ -17,7 +17,7 @@
     those of {!Matching.matching_result}), and a {!Term.constr}
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
-  subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ;
+  subst : Constr_matching.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 26fd773232..d52d2786d6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1979,7 +1979,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 ConstrMatching.PatternMatchingFailure
+      -> raise Constr_matching.PatternMatchingFailure
 
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter begin fun gl ->
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 46f2abd7f5..2c5edc20ed 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -20,7 +20,7 @@ Tacenv
 Hints
 Auto
 Tacintern
-TacticMatching
+Tactic_matching
 Tacinterp
 Evar_tactics
 Term_dnet