merge

3 files changed, 12 insertions, 14 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index b6dda93c22..08fd0186a0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_named_context_of env sigma =
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_named_context env sigma ne_context =
-  hv 0 (Context.fold_named_context
+  hv 0 (Context.Named.fold_outside
 	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
           ne_context ~init:(mt ()))
 
@@ -306,7 +306,7 @@ let pr_rel_context_of env sigma =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited env sigma =
   let sign_env =
-    Context.fold_named_list_context
+    Context.NamedList.fold
       (fun d pps ->
          let pidt =  pr_var_list_decl env sigma d in
          (pps ++ fnl () ++ pidt))
@@ -333,7 +333,7 @@ let pr_context_limit n env sigma =
   else
     let k = lgsign-n in
     let _,sign_env =
-      Context.fold_named_list_context
+      Context.NamedList.fold
         (fun d (i,pps) ->
            if i < k then
 	     (i+1, (pps ++str "."))
@@ -726,7 +726,7 @@ let prterm = pr_lconstr
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant     (* An opaque constant. *)
   | Transparent of constant
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 5c60b89366..bdb295a478 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -10,7 +10,6 @@ open Pp
 open Names
 open Globnames
 open Term
-open Context
 open Environ
 open Pattern
 open Evd
@@ -109,13 +108,13 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
 
-val pr_var_decl            : env -> evar_map -> named_declaration -> std_ppcmds
-val pr_var_list_decl       : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl            : env -> evar_map -> rel_declaration -> std_ppcmds
+val pr_var_decl            : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_var_list_decl       : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
 
-val pr_named_context       : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds
 val pr_named_context_of    : env -> evar_map -> std_ppcmds
-val pr_rel_context         : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context         : env -> evar_map -> Context.Rel.t -> std_ppcmds
 val pr_rel_context_of      : env -> evar_map -> std_ppcmds
 val pr_context_of          : env -> evar_map -> std_ppcmds
 
@@ -165,7 +164,7 @@ val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 type context_object =
   | Variable of Id.t  (** A section variable or a Let definition *)
   (** An axiom and the type it inhabits (if an axiom of the empty type) *)
-  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e0b1d55be2..3973c2db67 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -65,7 +65,6 @@ let get_new_id locals id =
 
 (** Inductive declarations *)
 
-open Context
 open Termops
 open Reduction
 
@@ -90,7 +89,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
+  let args = Context.Rel.to_extended_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -144,7 +143,7 @@ let print_record env mind mib =
   in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
+  let args = Context.Rel.to_extended_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in