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

1 files changed, 12 insertions, 8 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 94a7e37f4a..02fe6ce3a0 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -12,6 +12,9 @@ open Util
 open Glob_termops
 open Misctypes
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 let observe strm =
   if do_observe ()
   then Feedback.msg_debug strm
@@ -333,19 +336,20 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-	let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
-	let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
-        let open Context.Named.Declaration in
-	Environ.push_named (of_tuple (id,value,typ)) env
+        let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
+        (match raw_value with
+        | None ->
+           Environ.push_named (NamedDecl.LocalAssum (id,typ)) env
+        | Some value ->
+           Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env)
 
 
 let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
-    let open Context.Rel.Declaration in
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
     match pat with
-      | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env
+      | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
       | PatCstr(_,c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
 	    try Inductiveops.find_rectype env (Evd.from_env env) typ
@@ -353,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
 	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
-	  let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
+	  let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
 	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
   let new_env = add_pat_variables  env pat typ in
@@ -614,7 +618,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
           let open Context.Named.Declaration in
 	  match n with
 	      Anonymous -> env
-	    | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env
+	    | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
 	in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res