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

11 files changed, 82 insertions, 60 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index a047bf53c..7afd7a038 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -983,7 +983,10 @@ let rec mem_named_context id ctxt =
 
 let compact_named_context_reverse sign =
   let compact l decl =
-    let (i1,c1,t1) = NamedDecl.to_tuple decl in
+    let (i1,c1,t1) = match decl with
+                     | NamedDecl.LocalAssum (i,t) -> i,None,t
+                     | NamedDecl.LocalDef (i,c,t) -> i,Some c,t
+    in
     match l with
     | [] -> [[i1],c1,t1]
     | (l2,c2,t2)::q ->
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 4046ef7ae..01e37c7c1 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -13,6 +13,9 @@ open Util
 open Pp
 open Printer
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
     when the -ideslave option is passed to Coqtop. Currently CoqIDE is
@@ -133,7 +136,8 @@ let annotate phrase =
 (** Goal display *)
 
 let hyp_next_tac sigma env decl =
-  let (id,_,ast) = Context.Named.Declaration.to_tuple decl in
+  let id = NamedDecl.get_id decl in
+  let ast = NamedDecl.get_type decl in
   let id_s = Names.Id.to_string id in
   let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in
   [
@@ -191,10 +195,9 @@ let process_goal sigma g =
   in
   let process_hyp d (env,l) =
     let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
-    let d' = List.map (fun name -> let open Context.Named.Declaration in
-                                   match pi2 d with
-                                   | None -> LocalAssum (name, pi3 d)
-                                   | Some value -> LocalDef (name, value, pi3 d))
+    let d' = List.map (fun name -> match pi2 d with
+                                   | None -> NamedDecl.LocalAssum (name, pi3 d)
+                                   | Some value -> NamedDecl.LocalDef (name, value, pi3 d))
                       (pi1 d) in
       (List.fold_right Environ.push_named d' env,
        (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
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]) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0fea2ba22..2f73ddd30 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,7 +24,9 @@ open Globnames
 open Evd
 open Pretype_errors
 open Sigma.Notations
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 type unify_fun = transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
@@ -58,14 +60,13 @@ let eval_flexible_term ts env evd c =
       else None
   | Rel n ->
       (try match lookup_rel n env with
-           | LocalAssum _ -> None
-           | LocalDef (_,v,_) -> Some (lift n v)
+           | RelDecl.LocalAssum _ -> None
+           | RelDecl.LocalDef (_,v,_) -> Some (lift n v)
        with Not_found -> None)
   | Var id ->
       (try
 	 if is_transparent_variable ts id then
-           let open Context.Named.Declaration in
-	   lookup_named id env |> get_value
+	   lookup_named id env |> NamedDecl.get_value
 	 else None
        with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
@@ -394,7 +395,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     assert (match sk with [] -> true | _ -> false);
     let (na,c1,c'1) = destLambda term in
     let c = nf_evar evd c1 in
-    let env' = push_rel (LocalAssum (na,c)) env in
+    let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
@@ -600,7 +601,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
                let na = Nameops.name_max na1 na2 in
-	       evar_conv_x ts (push_rel (LocalDef (na,b,t)) env) i pbty c'1 c'2);
+	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
           let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
@@ -715,7 +716,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
            (fun i ->
 	     let c = nf_evar i c1 in
              let na = Nameops.name_max na1 na2 in
-	     evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i CONV c'1 c'2)]
+	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
     | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
@@ -774,7 +775,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                (fun i ->
  	         let c = nf_evar i c1 in
                  let na = Nameops.name_max n1 n2 in
-	         evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)]
+	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
 	    if Int.equal x1 x2 then
@@ -951,7 +952,6 @@ let choose_less_dependent_instance evk evd term args =
   | [] -> None
   | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
 
-open Context.Named.Declaration
 let apply_on_subterm env evdref f c t =
   let rec applyrec (env,(k,c) as acc) t =
     (* By using eq_constr, we make an approximation, for instance, we *)
@@ -962,7 +962,7 @@ let apply_on_subterm env evdref f c t =
       match kind_of_term t with
       | Evar (evk,args) when Evd.is_undefined !evdref evk ->
           let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
-          let g decl a = if is_local_assum decl then applyrec acc a else a in
+          let g decl a = if NamedDecl.is_local_assum decl then applyrec acc a else a in
           mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
       | _ ->
         map_constr_with_binders_left_to_right
@@ -982,14 +982,16 @@ let filter_possible_projections c ty ctxt args =
   List.map_i (fun i decl ->
     let () = assert (i < len) in
     let a = Array.unsafe_get args i in
-    (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
+    (match decl with
+     | NamedDecl.LocalAssum _ -> false
+     | NamedDecl.LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
     (* in u *)
     isRel a && Int.Set.mem (destRel a) fv1 ||
     isVar a && Id.Set.mem (destVar a) fv2 ||
-    Id.Set.mem (get_id decl) tyvars)
+    Id.Set.mem (NamedDecl.get_id decl) tyvars)
     0 ctxt
 
 let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
@@ -1020,10 +1022,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   let env_evar = evar_filtered_env evi in
   let sign = named_context_val env_evar in
   let ctxt = evar_filtered_context evi in
-  let instance = List.map mkVar (List.map get_id ctxt) in
+  let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in
 
   let rec make_subst = function
-  | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c ->
+  | decl'::ctxt', c::l, occs::occsl when isVarId (NamedDecl.get_id decl') c ->
       begin match occs with
       | Some _ ->
         error "Cannot force abstraction on identity instance."
@@ -1031,7 +1033,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         make_subst (ctxt',l,occsl)
       end
   | decl'::ctxt', c::l, occs::occsl ->
-      let (id,_,t) = to_tuple decl' in
+      let id = NamedDecl.get_id decl' in
+      let t = NamedDecl.get_type decl' in
       let evs = ref [] in
       let ty = Retyping.get_type_of env_rhs evd c in
       let filter' = filter_possible_projections c ty ctxt args in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6c8677855..c0a42ae7d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -632,13 +632,13 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
 	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
-      let evd,b_in_sign = match d with
-      | LocalAssum _ -> evd,None
+      let evd,d' = match d with
+      | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
       | LocalDef (_,b,_) ->
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
-          evd,Some b in
-      (push_named_context_val (Context.Named.Declaration.of_tuple (id,b_in_sign,t_in_sign)) sign, Filter.extend 1 filter,
+          evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
+      (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
        push_rel d env,evd,id::avoid))
diff --git a/printing/printer.ml b/printing/printer.ml
index 28fd92659..977746837 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -22,6 +22,9 @@ open Constrextern
 open Ppconstr
 open Declarations
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 let emacs_str s =
   if !Flags.print_emacs then s else ""
 let delayed_emacs_cmd s =
@@ -261,18 +264,21 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) =
   (pr_id id ++ hov 0 (pbody ++ ptyp))
 
 let pr_var_decl env sigma d =
-  pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d)
+  let d = match d with
+          | NamedDecl.LocalAssum (id,typ) -> id, None, typ
+          | NamedDecl.LocalDef (id,c,typ) -> id, Some c, typ
+  in
+  pr_var_decl_skel pr_id env sigma d
 
 let pr_var_list_decl env sigma (l,c,typ) =
   hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ))
 
 let pr_rel_decl env sigma decl =
-  let open Context.Rel.Declaration in
-  let na = get_name decl in
-  let typ = get_type decl in
+  let na = RelDecl.get_name decl in
+  let typ = RelDecl.get_type decl in
   let pbody = match decl with
-    | LocalAssum _ -> mt ()
-    | LocalDef (_,c,_) ->
+    | RelDecl.LocalAssum _ -> mt ()
+    | RelDecl.LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = pr_lconstr_env env sigma c in
 	let pb = if isCast c then surround pb else pb in
@@ -417,8 +423,7 @@ let pr_evgl_sign sigma evi =
   | None -> [], []
   | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi)
   in
-  let open Context.Named.Declaration in
-  let ids = List.rev_map get_id l in
+  let ids = List.rev_map NamedDecl.get_id l in
   let warn =
     if List.is_empty ids then mt () else
       (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6..39dff4aca 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -213,7 +213,7 @@ let split_sign hfrom hto l =
   let rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
     | d :: right ->
-        let hyp,_,typ = to_tuple d in
+        let hyp = get_id d in
       	if Id.equal hyp hfrom then
 	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
@@ -489,15 +489,16 @@ and mk_casegoals sigma goal goalacc p c =
 
 
 let convert_hyp check sign sigma d =
-  let id,b,bt = to_tuple d in
+  let id = get_id d in
+  let b = get_value d in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
     apply_to_hyp check sign id
       (fun _ d' _ ->
-        let _,c,ct = to_tuple d' in
+        let c = get_value d' in
         let env = Global.env_of_context sign in
-        if check && not (is_conv env sigma bt ct) then
+        if check && not (is_conv env sigma (get_type d) (get_type d')) then
 	  errorlabstrm "Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index caa9b328a..5b24a1fb2 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -35,12 +35,14 @@ let in_nameset =
 let rec close_fwd e s =
   let s' =
     List.fold_left (fun s decl ->
-      let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
-      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
-      let vty = global_vars_set e ty in
+      let vb = match decl with
+               | LocalAssum _ -> Id.Set.empty
+               | LocalDef (_,b,_) -> global_vars_set e b
+      in
+      let vty = global_vars_set e (get_type decl) in
       let vbty = Id.Set.union vb vty in
       if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
-      then Id.Set.add id (Id.Set.union s vbty) else s)
+      then Id.Set.add (get_id decl) (Id.Set.union s vbty) else s)
     s (named_context e)
     in
   if Id.Set.equal s s' then s else close_fwd e s'