Avoiding introducing yet another convention in naming files.

23 files changed, 45 insertions, 45 deletions

diff --git a/Makefile.common b/Makefile.common
index 7c98b64de..d752a5be9 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -68,7 +68,7 @@ CORESRCDIRS:=\
 PLUGINS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
-  cc 		funind 		firstorder 	Derive \
+  cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          decl_mode	btauto
 
 SRCDIRS:=\
@@ -190,7 +190,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
 	ascii_syntax_plugin.cma \
         string_syntax_plugin.cma )
 DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
-DERIVECMA:=plugins/Derive/derive_plugin.cma
+DERIVECMA:=plugins/derive/derive_plugin.cma
 
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
         $(QUOTECMA) $(RINGCMA) \
@@ -314,7 +314,7 @@ BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto)
 RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
 EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
 CCVO:=
-DERIVEVO:=$(call cat_vo_itarget, plugins/Derive)
+DERIVEVO:=$(call cat_vo_itarget, plugins/derive)
 
 PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
 	    $(FOURIERVO) $(CCVO) $(FUNINDVO) \
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2e61cb697..2f78c2e91 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -132,7 +132,7 @@ Recordops
 Evarconv
 Typing
 Patternops
-ConstrMatching
+Constr_matching
 Find_subterm
 Tacred
 Classops
diff --git a/plugins/Derive/Derive.v b/plugins/derive/Derive.v
index 0d5a93b03..0d5a93b03 100644
--- a/plugins/Derive/Derive.v
+++ b/plugins/derive/Derive.v
diff --git a/plugins/Derive/derive.ml b/plugins/derive/derive.ml
index 156c9771a..156c9771a 100644
--- a/plugins/Derive/derive.ml
+++ b/plugins/derive/derive.ml
diff --git a/plugins/Derive/derive.mli b/plugins/derive/derive.mli
index 5157c4a27..5157c4a27 100644
--- a/plugins/Derive/derive.mli
+++ b/plugins/derive/derive.mli
diff --git a/plugins/Derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mllib
index 5ee0fc6da..5ee0fc6da 100644
--- a/plugins/Derive/derive_plugin.mllib
+++ b/plugins/derive/derive_plugin.mllib
diff --git a/plugins/Derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 0721c675f..0721c675f 100644
--- a/plugins/Derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
diff --git a/plugins/Derive/vo.itarget b/plugins/derive/vo.itarget
index b48098219..b48098219 100644
--- a/plugins/Derive/vo.itarget
+++ b/plugins/derive/vo.itarget
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 64166a0de..1299c99ef 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -107,7 +107,7 @@ open Names
 open Term
 open Pattern
 open Patternops
-open ConstrMatching
+open Constr_matching
 open Tacmach
 (*i*)
 
diff --git a/pretyping/constrMatching.ml b/pretyping/constr_matching.ml
index ad4c678cb..ad4c678cb 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constr_matching.ml
diff --git a/pretyping/constrMatching.mli b/pretyping/constr_matching.mli
index a4e797dae..a4e797dae 100644
--- a/pretyping/constrMatching.mli
+++ b/pretyping/constr_matching.mli
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index b189360c0..25d17c7c9 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -20,7 +20,7 @@ Miscops
 Glob_ops
 Redops
 Patternops
-ConstrMatching
+Constr_matching
 Tacred
 Typeclasses_errors
 Typeclasses
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2064fb6e1..9a778e018 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -943,9 +943,9 @@ let simpl env sigma c = strong whd_simpl env sigma c
 
 let matches_head env sigma c t =
   match kind_of_term t with
-    | App (f,_) -> ConstrMatching.matches env sigma c f
-    | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst (Projection.constant p))
-    | _ -> raise ConstrMatching.PatternMatchingFailure
+    | App (f,_) -> Constr_matching.matches env sigma c f
+    | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p))
+    | _ -> raise Constr_matching.PatternMatchingFailure
 
 let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
 
@@ -980,7 +980,7 @@ let e_contextually byhead (occs,c) f env sigma t =
     try
       let subst =
         if byhead then matches_head env sigma c t 
-	else ConstrMatching.matches env sigma c t in
+	else Constr_matching.matches env sigma c t in
       let ok =
 	if nowhere_except_in then Int.List.mem !pos locs
 	else not (Int.List.mem !pos locs) in
@@ -996,7 +996,7 @@ let e_contextually byhead (occs,c) f env sigma t =
       end
       else
 	traverse_below nested envc t
-    with ConstrMatching.PatternMatchingFailure ->
+    with Constr_matching.PatternMatchingFailure ->
       traverse_below nested envc t
   and traverse_below nested envc t =
     (* when byhead, find other occurrences without matching again partial
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fe648e765..4088373ca 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -96,8 +96,8 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
-let pf_is_matching              = pf_apply ConstrMatching.is_matching_conv
-let pf_matches                  = pf_apply ConstrMatching.matches_conv
+let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
+let pf_matches                  = pf_apply Constr_matching.matches_conv
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -226,7 +226,7 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_betadeltaiota gl (pf_get_type_of gl t)
 
-  let pf_matches gl pat t = pf_apply ConstrMatching.matches_conv gl pat t
+  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
   let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
   let pf_compute gl t = pf_apply compute gl t
diff --git a/tactics/auto.ml b/tactics/auto.ml
index ef6c38bf6..fc4a459de 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 df8a018bb..70490722e 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 9740f6c1f..02d163aca 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 89f6fbc74..a3862de58 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 52fa2e4a2..f4b13bba8 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 989f07d67..abeb47c3b 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 26fd77323..d52d2786d 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 46f2abd7f..2c5edc20e 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
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 26e6416a9..6b0692679 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -112,7 +112,7 @@ let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
 (** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
 let rec pattern_filter pat ref env typ =
   let typ = strip_outer_cast typ in
-  if ConstrMatching.is_matching env Evd.empty pat typ then true
+  if Constr_matching.is_matching env Evd.empty pat typ then true
   else match kind_of_term typ with
   | Prod (_, _, typ)
   | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
@@ -120,7 +120,7 @@ let rec pattern_filter pat ref env typ =
 
 let rec head_filter pat ref env typ =
   let typ = strip_outer_cast typ in
-  if ConstrMatching.is_matching_head env Evd.empty pat typ then true
+  if Constr_matching.is_matching_head env Evd.empty pat typ then true
   else match kind_of_term typ with
   | Prod (_, _, typ)
   | LetIn (_, _, _, typ) -> head_filter pat ref env typ
@@ -149,7 +149,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
 
 let search_about_filter query gr env typ = match query with
 | GlobSearchSubPattern pat ->
-  ConstrMatching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
+  Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
 | GlobSearchString s ->
   String.string_contains ~where:(name_of_reference gr) ~what:s
 
@@ -288,11 +288,11 @@ let interface_search flags =
       toggle (Str.string_match regexp id 0) flag
     in
     let match_type (pat, flag) =
-      toggle (ConstrMatching.is_matching env Evd.empty pat constr) flag
+      toggle (Constr_matching.is_matching env Evd.empty pat constr) flag
     in
     let match_subtype (pat, flag) =
       toggle
-        (ConstrMatching.is_matching_appsubterm ~closed:false 
+        (Constr_matching.is_matching_appsubterm ~closed:false 
 	   env Evd.empty pat constr) flag
     in
     let match_module (mdl, flag) =