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 /proofs | |
| 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.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 |
2 files changed, 3 insertions, 3 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 -> |