From 6ccd28e53ad7694883e8174489bf333351fa407a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Mon, 8 Apr 2019 18:08:30 +0200 Subject: [PATCH] Remove calls to Global.env in Heads --- pretyping/heads.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 7590ac301b30..ef27ca9b4e15 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -33,17 +33,16 @@ type head_approximation = | NotImmediatelyComputableHead (* FIXME: maybe change interface here *) -let rec compute_head = function +let rec compute_head env = function | EvalConstRef cst -> - let env = Global.env() in let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in (match body with | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env c) | EvalVarRef id -> - (match Global.lookup_named id with + (match lookup_named id env with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> - kind_of_head (Global.env()) c + kind_of_head env c | _ -> RigidHead RigidOther) and kind_of_head env t = @@ -51,14 +50,14 @@ and kind_of_head env t = | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) | Var id -> - (try on_subterm k l b (compute_head (EvalVarRef id)) + (try on_subterm k l b (compute_head env (EvalVarRef id)) with Not_found -> (* a goal variable *) match lookup_named id env with | LocalDef (_,c,_) -> aux k l c b | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> - (try on_subterm k l b (compute_head (EvalConstRef cst)) + (try on_subterm k l b (compute_head env (EvalConstRef cst)) with Not_found -> CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++