diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-25 21:46:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-25 21:55:34 +0200 |
| commit | 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (patch) | |
| tree | f7860f13dc18938953ead65c63923aba117d890b /tactics/auto.ml | |
| parent | 12c803053572194c85e4c7b7f347175c7c335858 (diff) | |
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 15 |
1 files changed, 10 insertions, 5 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 |