diff options
| author | Pierre-Marie Pédrot | 2019-04-24 16:03:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | a5a89e8b623cd5822f59b854a45efc8236ae0087 (patch) | |
| tree | 8950d13c0d8f75c14724191d58f100c78206a4d3 | |
| parent | 4785156d31eb513b6e7fcb8dbab1c219da83612b (diff) | |
Logic.convert_hyp now takes an environment as an argument.
This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index f51f2ea5bc..3fcde56e76 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -548,10 +548,10 @@ and treat_case sigma goal ci lbrty lf acc' = (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags -let convert_hyp check sign sigma d = +let convert_hyp ~check env sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env_of_context sign in + let sign = Environ.named_context_val env in match lookup_named_ctxt id sign with | exception Not_found -> if check then error_no_such_hypothesis env sigma id diff --git a/proofs/logic.mli b/proofs/logic.mli index f99076db23..163d71f69c 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -62,7 +62,7 @@ type 'id move_location = val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t -val convert_hyp : bool -> Environ.named_context_val -> evar_map -> +val convert_hyp : check:bool -> Environ.env -> evar_map -> EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5e8869f9b0..5a19f95f90 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -168,7 +168,7 @@ let convert_hyp ?(check=true) d = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in - let sign = convert_hyp check (named_context_val env) sigma d in + let sign = convert_hyp ~check env sigma d in let env = reset_with_named_context sign env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ty @@ -728,7 +728,7 @@ let e_change_in_hyps ?(check=true) f args = raise (RefinerError (env, sigma, NoSuchHyp id)) in let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in - let sign = Logic.convert_hyp check (named_context_val env) sigma d in + let sign = Logic.convert_hyp ~check env sigma d in let env = reset_with_named_context sign env in (env, sigma) in |