CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function

3 files changed, 19 insertions, 23 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 499551406b..036abbdebb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -16,6 +16,7 @@ open Vars
 open Termops
 open Environ
 open Globnames
+open Context.Named.Declaration
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -745,11 +746,10 @@ let evars_of_term c =
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
-  List.fold_right (fun decl s ->
-    Option.fold_left (fun s t ->
-      Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term (NamedDecl.get_type decl))) (NamedDecl.get_value decl))
-    nc Evar.Set.empty
+  Context.Named.fold_outside
+    (NamedDecl.fold (fun constr s -> Evar.Set.union s (evars_of_term constr)))
+    nc
+    ~init:Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
   Evar.Set.union (evars_of_term evi.evar_concl)
@@ -1285,11 +1285,10 @@ let pr_meta_map mmap =
   prlist pr_meta_binding (metamap_to_list mmap)
 
 let pr_decl (decl,ok) =
-  let id = NamedDecl.get_id decl in
-  match NamedDecl.get_value decl with
-  | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
-  | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
-      print_constr c ++ str (if ok then ")" else "}")
+  match decl with
+  | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+  | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
+                           print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
   | Evar_kinds.QuestionMark _ -> str "underscore"
@@ -1400,11 +1399,11 @@ let pr_evar_universe_context ctx =
        h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
 
 let print_env_short env =
-  let pr_body n = function
-  | None -> pr_name n
-  | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
-  let pr_named_decl decl = pr_body (Name (NamedDecl.get_id decl)) (NamedDecl.get_value decl) in
-  let pr_rel_decl decl = pr_body (RelDecl.get_name decl) (RelDecl.get_value decl) in
+  let pr_rel_decl = function
+    | RelDecl.LocalAssum (n,_) -> pr_name n
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+  in
+  let pr_named_decl = pr_rel_decl % NamedDecl.to_rel in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcfd26185e..d078532b5d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1717,9 +1717,9 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
 let subst_one_var dep_proof_ok x =
   Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
-    let xval = pf_get_hyp x gl |> NamedDecl.get_value in
+    let decl = pf_get_hyp x gl in
     (* If x has a body, simply replace x with body and clear x *)
-    if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else
+    if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else
       (* Find a non-recursive definition for x *)
       let res =
         try
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index d2deb9e1eb..c5ddf71864 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -37,13 +37,10 @@ let contract env lc =
           l := (Vars.substl !l c') :: !l;
           env
       | _ ->
-          let t' = Vars.substl !l (RelDecl.get_type decl) in
-          let c' = Option.map (Vars.substl !l) (RelDecl.get_value decl) in
-          let na' = named_hd env t' (RelDecl.get_name decl) in
+          let t = Vars.substl !l (RelDecl.get_type decl) in
+          let decl = decl |> RelDecl.map_name (named_hd env t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
           l := (mkRel 1) :: List.map (Vars.lift 1) !l;
-          match c' with
-          | None -> push_rel (LocalAssum (na',t')) env
-          | Some c' -> push_rel (LocalDef (na',c',t')) env
+          push_rel decl env
   in
   let env = process_rel_context contract_context env in
   (env, List.map (Vars.substl !l) lc)