diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 24 | ||||
| -rw-r--r-- | tactics/tactics.ml | 30 | ||||
| -rw-r--r-- | tactics/tactics.mli | 10 |
4 files changed, 40 insertions, 28 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 8794557ef6..aa32e0e5c4 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1396,13 +1396,13 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl = | Some id, Some p -> cut_replacing id newt (Tacmach.refine p) | Some id, None -> - change_in_hyp None newt (id, InHypTypeOnly) + change_in_hyp None (fun env sigma -> sigma, newt) (id, InHypTypeOnly) | None, Some p -> let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in tclTHENLAST (Tacmach.internal_cut false name newt) (tclTHEN (Proofview.V82.of_tactic (Tactics.revert [name])) (Tacmach.refine p)) - | None, None -> change_in_concl None newt + | None, None -> change_in_concl None (fun env sigma -> sigma, newt) in tclTHEN (evartac undef) tac in let tac = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ca582c82fc..97cb50a286 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1710,13 +1710,11 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let (sigma,c_interp) = + let c_interp env sigma = if is_onhyps && is_onconcl - then pf_interp_type ist gl c - else pf_interp_constr ist gl c + then interp_type ist env sigma c + else interp_constr ist env sigma c in - tclTHEN - (tclEVARS sigma) (Tactics.change None c_interp (interp_clause ist (pf_env gl) cl)) gl end @@ -1728,16 +1726,14 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.tactic begin fun gl -> let sign,op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let env' = Environ.push_named_context sign env in - let (sigma',c_interp) = - try interp_constr ist env' sigma c - with e when to_catch e (* Hack *) -> - errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") + let c_interp env sigma = + let env' = Environ.push_named_context sign env in + try interp_constr ist env' sigma c + with e when to_catch e (* Hack *) -> + errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in - tclTHEN - (tclEVARS sigma') - (Tactics.change (Some op) c_interp (interp_clause ist env cl)) - gl + (Tactics.change (Some op) c_interp (interp_clause ist env cl)) + gl end end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c7fc4197eb..f65f295b21 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -345,19 +345,30 @@ let e_reduct_in_hyp redfun (id,where) gl = (e_pf_reduce_decl redfun where (pf_get_hyp gl id)) convert_hyp_no_check gl +type change_arg = env -> evar_map -> evar_map * constr + (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb t env sigma c = - let evd, b = infer_conv ~pb:cv_pb env sigma t c in - if b then evd, t - else - errorlabstrm "convert-check-hyp" (str "Not convertible.") - + let sigma, t' = t env sigma in + let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in + if b then sigma, t' + else raise ConstrMatching.PatternMatchingFailure + +let change_and_check_subst cv_pb subst t env sigma c = + let t' env sigma = + let sigma, t = t env sigma in + sigma, replace_vars (Id.Map.bindings subst) t + in change_and_check cv_pb t' env sigma c + (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb t = function - | None -> change_and_check cv_pb t + | None -> fun env sigma c -> + (try change_and_check cv_pb t env sigma c + with ConstrMatching.PatternMatchingFailure -> + errorlabstrm "convert-check-hyp" (str "Not convertible.")) | Some occl -> - e_contextually false occl - (fun subst -> change_and_check Reduction.CONV (replace_vars (Id.Map.bindings subst) t)) + e_contextually false occl + (fun subst -> change_and_check_subst Reduction.CONV subst t) let change_in_concl occl t = e_reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast) @@ -378,6 +389,9 @@ let change chg c cls gl = change_option (bind_change_occurrences occs chg) c None) cls gl +let change_concl t = + change_in_concl None (fun env sigma -> sigma, t) + (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl (red_product,REVERTcast) let red_in_hyp = reduct_in_hyp red_product diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6574d88c58..5951a4af8e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -117,12 +117,14 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr +type change_arg = env -> evar_map -> evar_map * constr + val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic val reduct_option : tactic_reduction * cast_kind -> goal_location -> tactic val reduct_in_concl : tactic_reduction * cast_kind -> tactic -val change_in_concl : (occurrences * constr_pattern) option -> constr -> - tactic -val change_in_hyp : (occurrences * constr_pattern) option -> constr -> +val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> tactic +val change_concl : constr -> tactic +val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> hyp_location -> tactic val red_in_concl : tactic val red_in_hyp : hyp_location -> tactic @@ -144,7 +146,7 @@ val unfold_in_hyp : val unfold_option : (occurrences * evaluable_global_reference) list -> goal_location -> tactic val change : - constr_pattern option -> constr -> clause -> tactic + constr_pattern option -> change_arg -> clause -> tactic val pattern_option : (occurrences * constr) list -> goal_location -> tactic val reduce : red_expr -> clause -> tactic |