diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 20:04:58 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 20:25:02 +0100 |
commit | bf1eef119ef8f0e6a2ae4b66165d6e22c1ce9236 (patch) | |
tree | eae73dd080b6a704922c3ffcf7b47ede9e13651f /tactics | |
parent | 4afb91237fa89fd9dc018a567382e34d6b1e616f (diff) |
Monotonizing Tactics.change_arg.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tacinterp.ml | 23 | ||||
-rw-r--r-- | tactics/tactics.ml | 10 | ||||
-rw-r--r-- | tactics/tactics.mli | 2 |
3 files changed, 22 insertions, 13 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1673aac0a..b3a17df36 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2147,16 +2147,20 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars sigma = + let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in + let sigma = Sigma.to_evar_map sigma in let ist = { ist with lfun = lfun' } in - if is_onhyps && is_onconcl - then interp_type ist (pf_env gl) sigma c - else interp_constr ist (pf_env gl) sigma c - in + let (sigma, c) = + if is_onhyps && is_onconcl + then interp_type ist (pf_env gl) sigma c + else interp_constr ist (pf_env gl) sigma c + in + Sigma.Unsafe.of_pair (c, sigma) + end } in (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)) gl end @@ -2171,16 +2175,19 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.tactic begin fun gl -> let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let c_interp patvars sigma = + let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in - try interp_constr ist env sigma c + try + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_constr ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) 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 + end } in (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) { gl with sigma = sigma } end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 62f306927..fc453cfaf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -642,10 +642,10 @@ let e_change_in_hyp redfun (id,where) = Sigma.Unsafe.of_pair (convert_hyp c, sigma) end } -type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr +type change_arg = Pattern.patvar_map -> constr Sigma.run -let make_change_arg c = - fun pats sigma -> (sigma, replace_vars (Id.Map.bindings pats) c) +let make_change_arg c pats = + { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma } let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -667,7 +667,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc = (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = - let sigma, t' = t sigma in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (t', sigma, p) = t.run sigma in + let sigma = Sigma.to_evar_map sigma in check_types env sigma mayneedglobalcheck deep t' c; let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d62d27ca3..8a4717b7b 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -125,7 +125,7 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic |