diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 15 | ||||
| -rw-r--r-- | tactics/hipattern.ml4 | 3 | ||||
| -rw-r--r-- | tactics/tacticMatching.ml | 4 |
3 files changed, 15 insertions, 7 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e7082a579..418fc62f0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1218,16 +1218,20 @@ si après Intros la conclusion matche le pattern. let (forward_interp_tactic, extern_interp) = Hook.make () let conclPattern concl pat tac = - let constr_bindings = + let constr_bindings env sigma = match pat with | None -> Proofview.tclUNIT Id.Map.empty | Some pat -> - try Proofview.tclUNIT (ConstrMatching.matches pat concl) + try + Proofview.tclUNIT (ConstrMatching.matches env sigma 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 + Proofview.Goal.raw_enter (fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + constr_bindings env sigma >>= fun constr_bindings -> + Hook.get forward_interp_tactic constr_bindings tac) (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) @@ -1461,7 +1465,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) if exists_evaluable_reference (pf_env gl) c then tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl else tclFAIL 0 (str"Unbound reference") gl) - | Extern tacast -> conclPattern concl p tacast + | Extern tacast -> + conclPattern concl p tacast in tclLOG dbg (fun () -> pr_autotactic t) tactic diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index e171c2147..84fcd6dee 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -245,6 +245,9 @@ let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] 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 match_with_equation t = if not (isApp t) then raise NoEquationFound; let (hdapp,args) = destApp t in diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index 0f48db676..fa1b7f158 100644 --- a/tactics/tacticMatching.ml +++ b/tactics/tacticMatching.ml @@ -228,7 +228,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Term p -> begin try - put_subst (ConstrMatching.extended_matches p term) <*> + put_subst (ConstrMatching.extended_matches E.env E.sigma p term) <*> return lhs with ConstrMatching.PatternMatchingFailure -> fail end @@ -247,7 +247,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 with_app_context p term) matching_error + map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) matching_error (** [rule_match_term term rule] matches the term [term] with the |