diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-06 19:59:28 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:26:34 +0100 |
commit | 258c8502eafd3e078a5c7478a452432b5c046f71 (patch) | |
tree | d4ce21b23a67056242410fbd78362213700af099 | |
parent | 77e638121b6683047be915da9d0499a58fcb6e52 (diff) |
Constr_matching API using EConstr.
-rw-r--r-- | ltac/tactic_matching.ml | 4 | ||||
-rw-r--r-- | plugins/quote/quote.ml | 2 | ||||
-rw-r--r-- | pretyping/constr_matching.ml | 105 | ||||
-rw-r--r-- | pretyping/constr_matching.mli | 3 | ||||
-rw-r--r-- | pretyping/tacred.ml | 9 | ||||
-rw-r--r-- | proofs/tacmach.ml | 6 | ||||
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
-rw-r--r-- | tactics/hipattern.ml | 4 | ||||
-rw-r--r-- | toplevel/search.ml | 10 |
10 files changed, 84 insertions, 63 deletions
diff --git a/ltac/tactic_matching.ml b/ltac/tactic_matching.ml index 43a58f6b2..58998c96e 100644 --- a/ltac/tactic_matching.ml +++ b/ltac/tactic_matching.ml @@ -233,7 +233,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Term p -> begin try - put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*> + put_subst (Constr_matching.extended_matches E.env E.sigma p (EConstr.of_constr term)) <*> return lhs with Constr_matching.PatternMatchingFailure -> fail end @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.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 (EConstr.of_constr term)) imatching_error (** [rule_match_term term rule] matches the term [term] with the diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index a13948f77..7b6d502b5 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -402,7 +402,7 @@ let quote_terms ivs lc = match l with | (lhs, rhs)::tail -> begin try - let s1 = Id.Map.bindings (matches (Global.env ()) Evd.empty rhs c) in + let s1 = Id.Map.bindings (matches (Global.env ()) Evd.empty rhs (EConstr.of_constr c)) in let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 in Termops.subst_meta s2 lhs diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 1261844a0..ecf6b1121 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -57,14 +57,15 @@ let warn_meta_collision = strbrk " and a metavariable of same name.") -let constrain n (ids, m as x) (names, terms as subst) = +let constrain sigma n (ids, m) (names, terms as subst) = + let open EConstr in try let (ids', m') = Id.Map.find n terms in - if List.equal Id.equal ids ids' && eq_constr m m' then subst + if List.equal Id.equal ids ids' && eq_constr sigma m (EConstr.of_constr m') then subst else raise PatternMatchingFailure with Not_found -> let () = if Id.Map.mem n names then warn_meta_collision n in - (names, Id.Map.add n x terms) + (names, Id.Map.add n (ids, EConstr.Unsafe.to_constr m) terms) let add_binders na1 na2 binding_vars (names, terms as subst) = match na1, na2 with @@ -82,8 +83,9 @@ let add_binders na1 na2 binding_vars (names, terms as subst) = let rec build_lambda sigma vars ctx m = match vars with | [] -> let len = List.length ctx in - lift (-1 * len) m + EConstr.Vars.lift (-1 * len) m | n :: vars -> + let open EConstr in (* change [ x1 ... xn y z1 ... zm |- t ] into [ x1 ... xn z1 ... zm |- lam y. t ] *) let len = List.length ctx in @@ -92,7 +94,7 @@ let rec build_lambda sigma vars ctx m = match vars with else if Int.equal i (pred n) then mkRel 1 else mkRel (i + 1) in - let m = substl (List.init len init) m in + let m = Vars.substl (List.init len init) m in let pre, suf = List.chop (pred n) ctx in match suf with | [] -> assert false @@ -100,7 +102,7 @@ let rec build_lambda sigma vars ctx m = match vars with let map i = if i > n then pred i else i in let vars = List.map map vars in (** Check that the abstraction is legal *) - let frels = free_rels sigma (EConstr.of_constr t) in + let frels = free_rels sigma t in let brels = List.fold_right Int.Set.add vars Int.Set.empty in let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in (** Create the abstraction *) @@ -123,41 +125,55 @@ let rec extract_bound_aux k accu frels ctx = match ctx with let extract_bound_vars frels ctx = extract_bound_aux 1 Id.Set.empty frels ctx -let dummy_constr = mkProp +let dummy_constr = EConstr.mkProp let make_renaming ids = function | (Name id, Name _, _) -> begin - try mkRel (List.index Id.equal id ids) + try EConstr.mkRel (List.index Id.equal id ids) with Not_found -> dummy_constr end | _ -> dummy_constr +let local_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + +let to_fix (idx, (nas, cs, ts)) = + let inj = EConstr.of_constr in + (idx, (nas, Array.map inj cs, Array.map inj ts)) + let merge_binding sigma allow_bound_rels ctx n cT subst = let c = match ctx with | [] -> (* Optimization *) ([], cT) | _ -> - let frels = free_rels sigma (EConstr.of_constr cT) in + let open EConstr in + let frels = free_rels sigma cT in if allow_bound_rels then let vars = extract_bound_vars frels ctx in let ordered_vars = Id.Set.elements vars in let rename binding = make_renaming ordered_vars binding in let renaming = List.map rename ctx in - (ordered_vars, substl renaming cT) + (ordered_vars, Vars.substl renaming cT) else let depth = List.length ctx in let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in if depth < min_elt then - ([], lift (- depth) cT) + ([], Vars.lift (- depth) cT) else raise PatternMatchingFailure in - constrain n c subst + constrain sigma n c subst let matches_core env sigma convert allow_partial_app allow_bound_rels (binding_vars,pat) c = + let open EConstr in let convref ref c = - match ref, kind_of_term c with + match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.id_eq id id' | ConstRef c, Const (c',_) -> Names.eq_constant c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' @@ -165,12 +181,12 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | _, _ -> (if convert then let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') (EConstr.of_constr c) + is_conv env sigma (EConstr.of_constr c') c else false) in let rec sorec ctx env subst p t = - let cT = strip_outer_cast sigma (EConstr.of_constr t) in - match p,kind_of_term cT with + let cT = EConstr.of_constr (strip_outer_cast sigma t) in + match p, EConstr.kind sigma cT with | PSoApp (n,args),m -> let fold (ans, seen) = function | PRel n -> @@ -179,9 +195,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | _ -> error "Only bound indices allowed in second order pattern matching." in let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in - let frels = free_rels sigma (EConstr.of_constr cT) in + let frels = free_rels sigma cT in if Int.Set.subset frels relset then - constrain n ([], build_lambda sigma relargs ctx cT) subst + constrain sigma n ([], build_lambda sigma relargs ctx cT) subst else raise PatternMatchingFailure @@ -219,15 +235,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in Array.fold_left2 (sorec ctx env) subst args1 args22 else (* Might be a projection on the right *) - match kind_of_term c2 with + match EConstr.kind sigma c2 with | Proj (pr, c) when not (Projection.unfolded pr) -> - (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr args2) in - sorec ctx env subst p term + (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in + sorec ctx env subst p (EConstr.of_constr term) with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _ -> raise PatternMatchingFailure) | PApp (c1,arg1), App (c2,arg2) -> - (match c1, kind_of_term c2 with + (match c1, EConstr.kind sigma c2 with | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure @@ -237,8 +253,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels with Invalid_argument _ -> raise PatternMatchingFailure else raise PatternMatchingFailure | _, Proj (pr,c) when not (Projection.unfolded pr) -> - (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr arg2) in - sorec ctx env subst p term + (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in + sorec ctx env subst p (EConstr.of_constr term) with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _, _ -> try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2 @@ -249,32 +265,32 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> - (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c2) [] in - sorec ctx env subst p term + (try let term = Retyping.expand_projection env sigma pr c2 [] in + sorec ctx env subst p (EConstr.of_constr term) with Retyping.RetypeError _ -> raise PatternMatchingFailure) | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) + sorec ((na1,na2,c2)::ctx) (Environ.push_rel (local_assum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) + sorec ((na1,na2,c2)::ctx) (Environ.push_rel (local_assum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) + sorec ((na1,na2,t2)::ctx) (Environ.push_rel (local_def (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> - let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in - let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in + let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in + let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in - if noccur_between 1 n b2 && noccur_between 1 n' b2' then - let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in + if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then + let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,EConstr.of_constr t)::l in let ctx_br = List.fold_left f ctx ctx_b2 in let ctx_br' = List.fold_left f ctx ctx_b2' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in @@ -306,8 +322,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in List.fold_left chk_branch chk_head br1 - | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst - | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst + | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst | _ -> raise PatternMatchingFailure in @@ -328,13 +344,14 @@ type matching_result = { m_sub : bound_ident_map * patvar_map; m_ctx : constr; } -let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) +let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=EConstr.Unsafe.to_constr c; } , (IStream.thunk n) ) let isPMeta = function PMeta _ -> true | _ -> false let matches_head env sigma pat c = + let open EConstr in let head = - match pat, kind_of_term c with + match pat, EConstr.kind sigma c with | PApp (c1,arg1), App (c2,arg2) -> if isPMeta c1 then c else let n1 = Array.length arg1 in @@ -345,6 +362,7 @@ let matches_head env sigma pat c = (* Tells if it is an authorized occurrence and if the instance is closed *) let authorized_occ env sigma partial_app closed pat c mk_ctx = + let open EConstr in try let subst = matches_core_closed env sigma false partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst) @@ -356,9 +374,10 @@ let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = + let open EConstr in let rec aux env c mk_ctx next = let here = authorized_occ env sigma partial_app closed pat c mk_ctx in - let next () = match kind_of_term c with + let next () = match EConstr.kind sigma c with | Cast (c1,k,c2) -> let next_mk_ctx = function | [c1] -> mk_ctx (mkCast (c1, k, c2)) @@ -370,21 +389,21 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) | _ -> assert false in - let env' = Environ.push_rel (LocalAssum (x,c1)) env in + let env' = Environ.push_rel (local_assum (x,c1)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | Prod (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) | _ -> assert false in - let env' = Environ.push_rel (LocalAssum (x,c1)) env in + let env' = Environ.push_rel (local_assum (x,c1)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in - let env' = Environ.push_rel (LocalDef (x,c1,t)) env in + let env' = Environ.push_rel (local_def (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> let topdown = true in @@ -440,8 +459,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in if partial_app then try - let term = Retyping.expand_projection env sigma p (EConstr.of_constr c') [] in - aux env term mk_ctx next + let term = Retyping.expand_projection env sigma p c' [] in + aux env (EConstr.of_constr term) mk_ctx next with Retyping.RetypeError _ -> next () else try_aux [env, c'] next_mk_ctx next diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index ee6c5141b..32bb48c93 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -10,6 +10,7 @@ open Names open Term +open EConstr open Environ open Pattern @@ -63,7 +64,7 @@ val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : constr } + m_ctx : Constr.t } (** [match_subterm n pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat]. *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index a3983737d..9581db23d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -962,9 +962,10 @@ let simpl env sigma c = strong whd_simpl env sigma c (* Reduction at specific subterms *) let matches_head env sigma c t = - match kind_of_term t with + let open EConstr in + match EConstr.kind sigma t with | App (f,_) -> Constr_matching.matches env sigma c f - | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) + | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, Univ.Instance.empty)) | _ -> raise Constr_matching.PatternMatchingFailure (** FIXME: Specific function to handle projections: it ignores what happens on the @@ -999,8 +1000,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> else try let subst = - if byhead then matches_head env sigma c t - else Constr_matching.matches env sigma c t in + if byhead then matches_head env sigma c (EConstr.of_constr t) + else Constr_matching.matches env sigma c (EConstr.of_constr t) in let ok = if nowhere_except_in then Int.List.mem !pos locs else not (Int.List.mem !pos locs) in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 148f9d675..5e9c0ba8e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -106,8 +106,8 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching = pf_apply Constr_matching.is_matching_conv -let pf_matches = pf_apply Constr_matching.matches_conv +let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c) +let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c) (********************************************) (* Definition of the most primitive tactics *) @@ -232,7 +232,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t + let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t) let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/tactics/auto.ml b/tactics/auto.ml index 17fe7362d..7462b8d85 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -139,7 +139,7 @@ let conclPattern concl pat tac = | None -> Proofview.tclUNIT Id.Map.empty | Some pat -> try - Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) + Proofview.tclUNIT (Constr_matching.matches env sigma pat (EConstr.of_constr concl)) with Constr_matching.PatternMatchingFailure -> Tacticals.New.tclZEROMSG (str "conclPattern") in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a31e581e8..bef43d20b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -305,7 +305,7 @@ let matches_pattern concl pat = | None -> Proofview.tclUNIT () | Some pat -> let sigma = Sigma.to_evar_map sigma in - if Constr_matching.is_matching env sigma pat concl then + if Constr_matching.is_matching env sigma pat (EConstr.of_constr concl) then Proofview.tclUNIT () else Tacticals.New.tclZEROMSG (str "conclPattern") diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a42a51fc0..d27e4afb7 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -276,8 +276,8 @@ let coq_refl_jm_pattern = open Globnames -let is_matching x y = is_matching (Global.env ()) Evd.empty x y -let matches x y = matches (Global.env ()) Evd.empty x y +let is_matching x y = is_matching (Global.env ()) Evd.empty x (EConstr.of_constr y) +let matches x y = matches (Global.env ()) Evd.empty x (EConstr.of_constr y) let match_with_equation t = if not (isApp t) then raise NoEquationFound; diff --git a/toplevel/search.ml b/toplevel/search.ml index c0bcc403c..653d4ac5c 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -113,7 +113,7 @@ let generic_search glnumopt fn = (** FIXME: this is quite dummy, we may find a more efficient algorithm. *) let rec pattern_filter pat ref env typ = let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in - if Constr_matching.is_matching env Evd.empty pat typ then true + if Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr typ) then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ @@ -121,7 +121,7 @@ let rec pattern_filter pat ref env typ = let rec head_filter pat ref env typ = let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in - if Constr_matching.is_matching_head env Evd.empty pat typ then true + if Constr_matching.is_matching_head env Evd.empty pat (EConstr.of_constr 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 -> - Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ + Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat (EConstr.of_constr typ) | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s @@ -265,12 +265,12 @@ let interface_search = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (Constr_matching.is_matching env Evd.empty pat constr) flag + toggle (Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr constr)) flag in let match_subtype (pat, flag) = toggle (Constr_matching.is_matching_appsubterm ~closed:false - env Evd.empty pat constr) flag + env Evd.empty pat (EConstr.of_constr constr)) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag |