diff options
| -rw-r--r-- | engine/termops.ml | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
| -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 | ||||
| -rw-r--r-- | printing/prettyp.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | toplevel/assumptions.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
13 files changed, 21 insertions, 21 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 501a7dfa4..b2c9492e1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1002,7 +1002,7 @@ let compact_named_context sign = | NamedDecl.LocalDef (i,c,t), q -> CompactedDecl.LocalDef ([i],c,t) :: q in - Context.Named.fold_inside compact ~init:[] sign |> List.rev + sign |> Context.Named.fold_inside compact ~init:[] |> List.rev let clear_named_body id env = let open NamedDecl in diff --git a/library/impargs.ml b/library/impargs.ml index e922ab773..2997f94ed 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -175,7 +175,7 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - Environ.lookup_named id env |> is_local_def + env |> Environ.lookup_named id |> is_local_def | Ind _ | Construct _ -> false | _ -> true diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 8e6c7a70d..90adb0c36 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -824,7 +824,7 @@ let define_tac id args body gls = let cast_tac id_or_thesis typ gls = match id_or_thesis with | This id -> - Proofview.V82.of_tactic (pf_get_hyp gls id |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls + Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e745824b8..31fb1174a 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 ffb9f8940..1e5f12b20 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 f044e919b..9b4415920 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 c1d4a3403..160b3bc3f 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 diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 37098e504..f56f83e17 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -763,7 +763,7 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - lookup_named id env |> NamedDecl.set_id id |> print_named_decl + env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 957843bc9..e90024076 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -59,7 +59,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - pf_get_hyp gls id |> NamedDecl.get_type + id |> pf_get_hyp gls |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 8c43ac8b5..1672b7bd1 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -565,7 +565,7 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = - try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in + try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) not (Term.eq_constr t (NamedDecl.get_type hyp)) with Not_found -> true diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7ee45523f..51bbd9058 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2783,7 +2783,7 @@ let old_generalize_dep ?(with_let=false) c gl = let body = if with_let then match kind_of_term c with - | Var id -> Tacmach.pf_get_hyp gl id |> NamedDecl.get_value + | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value | _ -> None else None in @@ -3561,7 +3561,7 @@ let linear vars args = with Seen -> false let is_defined_variable env id = - lookup_named id env |> is_local_def + env |> lookup_named id |> is_local_def let abstract_args gl generalize_vars dep id defined f args = let open Context.Rel.Declaration in diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 49a815dc1..8865cd646 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -146,7 +146,7 @@ let label_of = function let rec traverse current ctx accu t = match kind_of_term t with | Var id -> - let body () = Global.lookup_named id |> NamedDecl.get_value in + let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> let body () = Global.body_of_constant_body (lookup_constant kn) in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c5ddf7186..670d30c6c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -148,7 +148,7 @@ let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags let pr_db env i = try - match lookup_rel i env |> get_name with + match env |> lookup_rel i |> get_name with | Name id -> pr_id id | Anonymous -> str "<>" with Not_found -> str "UNBOUND_REL_" ++ int i |