CLEANUP: using |> operator more consistently

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