aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib2
-rw-r--r--plugins/quote/quote.ml2
-rw-r--r--pretyping/constrMatching.ml (renamed from pretyping/matching.ml)3
-rw-r--r--pretyping/constrMatching.mli (renamed from pretyping/matching.mli)0
-rw-r--r--pretyping/pretyping.mllib2
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--tactics/auto.ml11
-rw-r--r--tactics/eqdecide.ml42
-rw-r--r--tactics/equality.ml19
-rw-r--r--tactics/hipattern.ml42
-rw-r--r--tactics/tacinterp.ml3
-rw-r--r--tactics/tacticMatching.ml16
-rw-r--r--tactics/tacticMatching.mli2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--toplevel/search.ml11
16 files changed, 45 insertions, 46 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 82ef43a7d5..30ac772d0a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -118,7 +118,7 @@ Evarconv
Arguments_renaming
Typing
Patternops
-Matching
+ConstrMatching
Tacred
Classops
Typeclasses_errors
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 21b221318e..affe31d790 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -107,7 +107,7 @@ open Names
open Term
open Pattern
open Patternops
-open Matching
+open ConstrMatching
open Tacmach
open Proofview.Notations
(*i*)
diff --git a/pretyping/matching.ml b/pretyping/constrMatching.ml
index 0d3f249281..45b097c003 100644
--- a/pretyping/matching.ml
+++ b/pretyping/constrMatching.ml
@@ -219,7 +219,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
let s' =
List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in
let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
- sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
+ sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
else
raise PatternMatchingFailure
@@ -407,4 +407,3 @@ let matches_conv env sigma c p =
let is_matching_conv env sigma pat n =
try let _ = matches_conv env sigma pat n in true
with PatternMatchingFailure -> false
-
diff --git a/pretyping/matching.mli b/pretyping/constrMatching.mli
index b82f115251..b82f115251 100644
--- a/pretyping/matching.mli
+++ b/pretyping/constrMatching.mli
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index d4892f2f8a..469be6d9ea 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -20,7 +20,7 @@ Miscops
Glob_ops
Redops
Patternops
-Matching
+ConstrMatching
Tacred
Typeclasses_errors
Typeclasses
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 46037e5eee..4b03c935f5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -22,7 +22,6 @@ open Closure
open Reductionops
open Cbv
open Patternops
-open Matching
open Locus
(* Errors *)
@@ -804,8 +803,8 @@ let simpl env sigma c = strong whd_simpl env sigma c
let matches_head c t =
match kind_of_term t with
- | App (f,_) -> matches c f
- | _ -> raise PatternMatchingFailure
+ | App (f,_) -> ConstrMatching.matches c f
+ | _ -> raise ConstrMatching.PatternMatchingFailure
let contextually byhead (occs,c) f env sigma t =
let (nowhere_except_in,locs) = Locusops.convert_occs occs in
@@ -815,7 +814,8 @@ let contextually byhead (occs,c) f env sigma t =
if nowhere_except_in && (!pos > maxocc) then t
else
try
- let subst = if byhead then matches_head c t else matches c t in
+ let subst =
+ if byhead then matches_head c t else ConstrMatching.matches c t in
let ok =
if nowhere_except_in then Int.List.mem !pos locs
else not (Int.List.mem !pos locs) in
@@ -829,7 +829,7 @@ let contextually byhead (occs,c) f env sigma t =
mkApp (f, Array.map_left (traverse envc) l)
else
t
- with PatternMatchingFailure ->
+ with ConstrMatching.PatternMatchingFailure ->
map_constr_with_binders_left_to_right
(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
traverse envc t
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c0875d756f..de73f7720d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -102,8 +102,8 @@ let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
let pf_check_type gls c1 c2 =
ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
-let pf_is_matching = pf_apply Matching.is_matching_conv
-let pf_matches = pf_apply Matching.matches_conv
+let pf_is_matching = pf_apply ConstrMatching.is_matching_conv
+let pf_matches = pf_apply ConstrMatching.matches_conv
(************************************)
(* Tactics handling a list of goals *)
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
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 91762c0003..78fa3a325d 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -114,7 +114,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 Matching.is_matching pat typ then true
+ if ConstrMatching.is_matching pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
| LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
@@ -122,7 +122,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 Matching.is_matching_head pat typ then true
+ if ConstrMatching.is_matching_head pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
| LetIn (_, _, _, typ) -> head_filter pat ref env typ
@@ -151,7 +151,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 ->
- Matching.is_matching_appsubterm ~closed:false pat typ
+ ConstrMatching.is_matching_appsubterm ~closed:false pat typ
| GlobSearchString s ->
String.string_contains ~where:(name_of_reference gr) ~what:s
@@ -277,10 +277,11 @@ let interface_search flags =
toggle (Str.string_match regexp id 0) flag
in
let match_type (pat, flag) =
- toggle (Matching.is_matching pat constr) flag
+ toggle (ConstrMatching.is_matching pat constr) flag
in
let match_subtype (pat, flag) =
- toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag
+ toggle
+ (ConstrMatching.is_matching_appsubterm ~closed:false pat constr) flag
in
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:27:22 +0000