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

2 files changed, 23 insertions, 20 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0fea2ba223..2f73ddd30c 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 6c8677855a..c0a42ae7d3 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))