diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 14 |
4 files changed, 11 insertions, 11 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e745824b8a..31fb1174a4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -67,7 +67,7 @@ let eval_flexible_term ts env evd c = | Var id -> (try if is_transparent_variable ts id then - lookup_named id env |> NamedDecl.get_value + env |> lookup_named id |> NamedDecl.get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index ffb9f8940a..1e5f12b209 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -124,7 +124,7 @@ let build_case_type dep p realargs c = (* TODO move this function *) let type_of_rel env n = - lookup_rel n env |> RelDecl.get_type |> lift n + env |> lookup_rel n |> RelDecl.get_type |> lift n let type_of_prop = mkSort type1_sort @@ -135,7 +135,7 @@ let type_of_sort s = let type_of_var env id = let open Context.Named.Declaration in - try lookup_named id env |> get_type + try env |> lookup_named id |> get_type with Not_found -> anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound") diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f044e919b5..9b44159200 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1058,7 +1058,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try - let t' = lookup_named id env |> NamedDecl.get_type in + let t' = env |> lookup_named id |> NamedDecl.get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c1d4a34038..160b3bc3f4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -62,7 +62,7 @@ let value_of_evaluable_ref env evref u = (try constant_value_in env (con,u) with NotEvaluableConst IsProj -> raise (Invalid_argument "value_of_evaluable_ref")) - | EvalVarRef id -> lookup_named id env |> NamedDecl.get_value |> Option.get + | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst @@ -114,18 +114,18 @@ let unsafe_reference_opt_value env sigma eval = | Declarations.Def c -> Some (Mod_subst.force_constr c) | _ -> None) | EvalVar id -> - lookup_named id env |> NamedDecl.get_value + env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> - lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value + env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value | EvalEvar ev -> Evd.existential_opt_value sigma ev let reference_opt_value env sigma eval u = match eval with | EvalConst cst -> constant_opt_value_in env (cst,u) | EvalVar id -> - lookup_named id env |> NamedDecl.get_value + env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> - lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value + env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value | EvalEvar ev -> Evd.existential_opt_value sigma ev exception NotEvaluable @@ -539,9 +539,9 @@ let match_eval_ref_value env sigma constr = | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> Some (constant_value_in env (sp, u)) | Var id when is_evaluable env (EvalVarRef id) -> - lookup_named id env |> NamedDecl.get_value + env |> lookup_named id |> NamedDecl.get_value | Rel n -> - lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value + env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value | Evar ev -> Evd.existential_opt_value sigma ev | _ -> None |