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

4 files changed, 23 insertions, 18 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index fd46d8069..930ab333a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,7 +23,9 @@ open Pp
 open CErrors
 open Util
 open Proofview.Notations
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
@@ -155,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff
+	  quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
@@ -170,7 +172,7 @@ let litteral_of_constr env sigma term=
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff
+	      quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
@@ -192,10 +194,10 @@ let make_prb gls depth additionnal_terms =
 	   ignore (add_term state t)) additionnal_terms;
     List.iter
       (fun decl ->
-         let (id,_,e) = Context.Named.Declaration.to_tuple decl in
+         let id = NamedDecl.get_id decl in
 	 begin
 	   let cid=mkVar id in
-	   match litteral_of_constr env sigma e with
+	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
 	     | `Other ph ->
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97c9d5f4a..6a28723b8 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -821,9 +821,8 @@ let define_tac id args body gls =
 
 let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
-      This id ->
-	let body = pf_get_hyp gls id |> get_value in
-	  Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls
+    | This id ->
+        Proofview.V82.of_tactic  (pf_get_hyp gls id |> set_id id |> set_type typ |> convert_hyp) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 94a7e37f4..02fe6ce3a 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
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d625e3076..c5c44ef20 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1697,8 +1697,8 @@ let destructure_hyps =
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
       | decl::lit ->
-          let (i,_,t) = to_tuple decl in
-	  begin try match destructurate_prop t with
+          let i = get_id decl in
+	  begin try match destructurate_prop (get_type decl) with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->