merge

13 files changed, 112 insertions, 120 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d6552920f..726422c6f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
-          let hyp = Context.map_named_declaration nf decl in
+          let hyp = Context.Named.Declaration.map nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list
 	       (Hint_db.add_list env sigma hintl local_db)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 64a68ba6b..2c713a021 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -49,7 +49,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
 open Inductive
@@ -71,8 +70,8 @@ let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt
-       @ extended_rel_list 0 realargs)
+       Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt
+       @ Context.Rel.to_extended_list 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
@@ -109,7 +108,7 @@ let get_sym_eq_data env (ind,u) =
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
   let params,constrargs = List.chop mib.mind_nparams constrargs in
   if mip.mind_nrealargs > mib.mind_nparams then
@@ -144,7 +143,7 @@ let get_non_sym_eq_data env (ind,u) =
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
   let _,constrargs = List.chop mib.mind_nparams constrargs in
   let constrargs = List.map (Vars.subst_instance_constr u) constrargs in
@@ -170,7 +169,7 @@ let build_sym_scheme env ind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
@@ -183,7 +182,7 @@ let build_sym_scheme env ind =
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkApp (mkIndU indu,Array.concat
-	  [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	  [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 	   rel_vect 1 nrealargs;
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
@@ -224,13 +223,13 @@ let build_sym_involutive_scheme env ind =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in
+  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
       (mkIndU indu, Array.append
-         (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt)
+         (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
@@ -244,15 +243,15 @@ let build_sym_involutive_scheme env ind =
 	       (mkApp (eq,[|
 	       mkApp
 	       (mkIndU indu, Array.concat
-	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		rel_vect (2*nrealargs+2) nrealargs;
 		rel_vect 1 nrealargs]);
                mkApp (sym,Array.concat
-	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		rel_vect 1 nrealargs;
 		rel_vect (2*nrealargs+2) nrealargs;
 		[|mkApp (sym,Array.concat
-		[extended_rel_vect (3*nrealargs+2) paramsctxt1;
+		[Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		 rel_vect (2*nrealargs+2) nrealargs;
 		 rel_vect 1 nrealargs;
 		 [|mkRel 1|]])|]]);
@@ -335,7 +334,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [extended_rel_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -343,12 +342,12 @@ let build_l2r_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect nrealargs nrealargs]) in
   let applied_ind_G =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs+3) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1;
         rel_vect (nrealargs+3) nrealargs;
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
@@ -359,10 +358,10 @@ let build_l2r_rew_scheme dep env ind kind =
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
-       Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+       Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
   let applied_sym_G =
      mkApp(sym,
-       Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1;
+       Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1;
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
@@ -372,7 +371,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
   let applied_PC =
-    mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign)
+    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
   let applied_PG =
     mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
@@ -382,11 +381,11 @@ let build_l2r_rew_scheme dep env ind kind =
            (if dep then [|mkRel 2|] else [||])) in
   let applied_sym_sym =
          mkApp (sym,Array.concat
-	   [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	   [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
             rel_vect 4 nrealargs;
             rel_vect (nrealargs+4) nrealargs;
             [|mkApp (sym,Array.concat
-	      [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	      [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
 	       rel_vect (nrealargs+4) nrealargs;
 	       rel_vect 4 nrealargs;
 	       [|mkRel 2|]])|]]) in
@@ -409,7 +408,7 @@ let build_l2r_rew_scheme dep env ind kind =
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
        mkApp (sym_involutive,
-         Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+         Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
    else
      main_body))))))
@@ -448,7 +447,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     get_sym_eq_data env indu in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [extended_rel_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -456,12 +455,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (4*nrealargs+2) paramsctxt1;
+       [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (nrealargs+1) nrealargs]) in
   let applied_ind_P' =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs+1) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
@@ -539,7 +538,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -555,8 +554,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
     mkApp (mkVar varP,
-           if dep then extended_rel_vect 0 realsign_ind
-	   else extended_rel_vect 1 realsign) in
+           if dep then Context.Rel.to_extended_vect 0 realsign_ind
+	   else Context.Rel.to_extended_vect 1 realsign) in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -600,12 +599,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
   | hp :: p :: ind :: indargs ->
      let c' = 
       my_it_mkLambda_or_LetIn indargs
-	(mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p)
-	  (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp)
-	    (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind)
+	(mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p)
+	  (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp)
+	    (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind)
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
-	          extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
+	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
@@ -744,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind =
   let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
+  if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
   let varB = fresh env (Id.of_string "B") in
@@ -760,8 +759,8 @@ let build_congr env (eq,refl,ctx) ind =
      (mkNamedLambda varH
         (applist
            (mkIndU indu,
-	    extended_rel_list (mip.mind_nrealargs+2) paramsctxt @
-	    extended_rel_list 0 realsign))
+	    Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @
+	    Context.Rel.to_extended_list 0 realsign))
      (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
 	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
@@ -769,9 +768,9 @@ let build_congr env (eq,refl,ctx) ind =
            (Anonymous,
             applist
              (mkIndU indu,
-	        extended_rel_list (2*mip.mind_nrealdecls+3)
+	        Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3)
 		  paramsctxt
-	        @ extended_rel_list 0 realsign),
+	        @ Context.Rel.to_extended_list 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1854b4120..ac41c9464 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1574,7 +1574,7 @@ let unfold_body x =
   Proofview.Goal.enter { enter = begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let (_, xval, _) = Context.lookup_named x hyps in
+  let (_, xval, _) = Context.Named.lookup x hyps in
   let xval = match xval with
   | None -> errorlabstrm "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
@@ -1656,7 +1656,7 @@ let subst_one_var dep_proof_ok x =
           (** [is_eq_x] ensures nf_evar on its side *)
           let hyps = Proofview.Goal.hyps gl in
           let test hyp _ = is_eq_x gl varx hyp in
-          Context.fold_named_context test ~init:() hyps;
+          Context.Named.fold_outside test ~init:() hyps;
           errorlabstrm "Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a957a5624..15765bab5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -323,7 +323,7 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in
+  let c = Reductionops.whd_beta Evd.empty (mkApp (c, Context.Rel.to_extended_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 257598d18..c9187f54a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -10,7 +10,6 @@ open Pp
 open Util
 open Names
 open Term
-open Context
 open Environ
 open Globnames
 open Decl_kinds
@@ -192,7 +191,7 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp :
-  env -> evar_map -> named_declaration -> hint_entry list
+  env -> evar_map -> Context.Named.Declaration.t -> hint_entry list
 
 (** [make_extern pri pattern tactic_expr] *)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ed1a62795..3574990f6 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Termops
 open Namegen
 open Environ
@@ -97,7 +96,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
   in
-  let nhyps = rel_context_length hyps in
+  let nhyps = Context.Rel.length hyps in
   let env' = push_rel_context hyps env in
   (* Now the arity is pushed, and we need to construct the pairs
    * ai,mkRel(n-i+1) *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 75e69bc09..9154c50c8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -14,7 +14,6 @@ open Term
 open Vars
 open Termops
 open Namegen
-open Context
 open Evd
 open Printer
 open Reductionops
@@ -157,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
 	fold_named_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
              if Id.List.mem id ivars then
-	       ((mkVar id)::revargs,add_named_decl d hyps)
+	       ((mkVar id)::revargs, Context.Named.add d hyps)
 	     else
 	       (revargs,hyps))
           env ~init:([],[])
@@ -206,8 +205,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     fold_named_context
       (fun env (id,_,_ as d) sign ->
          if mem_named_context id global_named_context then sign
-	 else add_named_decl d sign)
-      invEnv ~init:empty_named_context
+	 else Context.Named.add d sign)
+      invEnv ~init:Context.Named.empty
   end in
   let avoid = ref [] in
   let { sigma=sigma } = Proof.V82.subgoals pf in
@@ -218,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
-	ownSign := add_named_decl (h,None,ty) !ownSign;
+	ownSign := Context.Named.add (h,None,ty) !ownSign;
 	applist (mkVar h, inst)
     | _ -> map_constr fill_holes c
   in
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 40a18ac45..1de47b2be 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -71,7 +71,7 @@ val cl_rewrite_clause :
   bool -> Locus.occurrences -> Id.t option -> tactic
 
 val is_applied_rewrite_relation :
-  env -> evar_map -> Context.rel_context -> constr -> types option
+  env -> evar_map -> Context.Rel.t -> constr -> types option
 
 val declare_relation :
   ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t ->
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
index d8e6dd0ae..090207bcc 100644
--- a/tactics/tactic_matching.mli
+++ b/tactics/tactic_matching.mli
@@ -43,7 +43,7 @@ val match_term :
 val match_goal:
   Environ.env ->
   Evd.evar_map ->
-  Context.named_context ->
+  Context.Named.t ->
   Term.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 74714300c..750ec8fb1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Term
 open Termops
-open Context
 open Declarations
 open Tacmach
 open Clenv
@@ -154,8 +153,8 @@ type branch_args = {
   branchnames : Tacexpr.intro_patterns}
 
 type branch_assumptions = {
-  ba        : branch_args;     (* the branch args *)
-  assums    : named_context}   (* the list of assumptions introduced *)
+  ba        : branch_args;       (* the branch args *)
+  assums    : Context.Named.t}   (* the list of assumptions introduced *)
 
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 042f80fe8..147f1f0f2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,7 +9,6 @@
 open Pp
 open Names
 open Term
-open Context
 open Tacmach
 open Proof_type
 open Tacexpr
@@ -60,29 +59,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
 val onNthHypId       : int -> (Id.t -> tactic) -> tactic
 val onNthHyp         : int -> (constr -> tactic) -> tactic
-val onNthDecl        : int -> (named_declaration -> tactic) -> tactic
+val onNthDecl        : int -> (Context.Named.Declaration.t -> tactic) -> tactic
 val onLastHypId      : (Id.t -> tactic) -> tactic
 val onLastHyp        : (constr -> tactic) -> tactic
-val onLastDecl       : (named_declaration -> tactic) -> tactic
+val onLastDecl       : (Context.Named.Declaration.t -> tactic) -> tactic
 val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
 val onNLastHyps      : int -> (constr list -> tactic) -> tactic
-val onNLastDecls     : int -> (named_context -> tactic) -> tactic
+val onNLastDecls     : int -> (Context.Named.t -> tactic) -> tactic
 
 val lastHypId   : goal sigma -> Id.t
 val lastHyp     : goal sigma -> constr
-val lastDecl    : goal sigma -> named_declaration
+val lastDecl    : goal sigma -> Context.Named.Declaration.t
 val nLastHypsId : int -> goal sigma -> Id.t list
 val nLastHyps   : int -> goal sigma -> constr list
-val nLastDecls  : int -> goal sigma -> named_context
+val nLastDecls  : int -> goal sigma -> Context.Named.t
 
-val afterHyp    : Id.t -> goal sigma -> named_context
+val afterHyp    : Id.t -> goal sigma -> Context.Named.t
 
 val ifOnHyp     : (Id.t * types -> bool) ->
                   (Id.t -> tactic) -> (Id.t -> tactic) ->
 		   Id.t -> tactic
 
-val onHyps      : (goal sigma -> named_context) ->
-                  (named_context -> tactic) -> tactic
+val onHyps      : (goal sigma -> Context.Named.t) ->
+                  (Context.Named.t -> tactic) -> tactic
 
 (** {6 Tacticals applying to goal components } *)
 
@@ -99,18 +98,18 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
 (** {6 Elimination tacticals. } *)
 
 type branch_args = {
-  ity        : pinductive;   (** the type we were eliminating on *)
+  ity        : pinductive;  (** the type we were eliminating on *)
   largs      : constr list; (** its arguments *)
   branchnum  : int;         (** the branch number *)
   pred       : constr;      (** the predicate we used *)
   nassums    : int;         (** the number of assumptions to be introduced *)
   branchsign : bool list;   (** the signature of the branch.
-                               true=recursive argument, false=constant *)
+                                true=recursive argument, false=constant *)
   branchnames : intro_patterns}
 
 type branch_assumptions = {
-  ba        : branch_args;     (** the branch args *)
-  assums    : named_context}   (** the list of assumptions introduced *)
+  ba        : branch_args;       (** the branch args *)
+  assums    : Context.Named.t}   (** the list of assumptions introduced *)
 
 (** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
    error message if |pats| <> n *)
@@ -224,7 +223,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context
+  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
@@ -233,11 +232,11 @@ module New : sig
   val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
   val onLastHypId      : (identifier -> unit tactic) -> unit tactic
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
-  val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
+  val onLastDecl       : (Context.Named.Declaration.t -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `NF ], named_context) Proofview.Goal.enter ->
-                    (named_context -> unit tactic) -> unit tactic
-  val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
+  val onHyps      : ([ `NF ], Context.Named.t) Proofview.Goal.enter ->
+                    (Context.Named.t -> unit tactic) -> unit tactic
+  val afterHyp    : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic
 
   val tryAllHyps          : (identifier -> unit tactic) -> unit tactic
   val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1349d5517..588bdc8ed 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Termops
 open Find_subterm
 open Namegen
@@ -1405,7 +1404,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist (elim,params@[t;branch]) in
-	let c = beta_applist (abselim, [mkApp (c, extended_rel_vect 0 sign)]) in
+	let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in
 	  Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
       else
 	None
@@ -1413,7 +1412,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       (* goes from left to right when i increases! *)
       match List.nth l i with
       | Some proj ->
-	  let args = extended_rel_vect 0 sign in
+	  let args = Context.Rel.to_extended_vect 0 sign in
 	  let proj =
 	    if Environ.is_projection proj env then
 	      mkProj (Projection.make proj false, mkApp (c, args))
@@ -1942,7 +1941,7 @@ let bring_hyps hyps =
       let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
-      let args = Array.of_list (instance_from_named_context hyps) in
+      let args = Array.of_list (Context.Named.to_instance hyps) in
       Proofview.Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -2568,7 +2567,7 @@ let generalize_dep ?(with_let=false) c gl =
       d::toquant
     else
       toquant in
-  let to_quantify = Context.fold_named_context seek sign ~init:[] in
+  let to_quantify = Context.Named.fold_outside seek sign ~init:[] in
   let to_quantify_rev = List.rev to_quantify in
   let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
   let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
@@ -2588,7 +2587,7 @@ let generalize_dep ?(with_let=false) c gl =
   in
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
-  let args = instance_from_named_context to_quantify_rev in
+  let args = Context.Named.to_instance to_quantify_rev in
   tclTHENLIST
     [tclEVARS evd;
      Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
@@ -2710,7 +2709,7 @@ let specialize (c,lbind) =
 let unfold_body x gl =
   let hyps = pf_hyps gl in
   let xval =
-    match Context.lookup_named x hyps with
+    match Context.Named.lookup x hyps with
         (_,Some xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
@@ -3131,20 +3130,20 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
-  nparams: int;            (* number of parameters *)
-  predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
-  npredicates: int;        (* Number of predicates *)
-  branches: rel_context;   (* branchr,...,branch1 *)
-  nbranches: int;          (* Number of branches *)
-  args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
-  nargs: int;              (* number of arguments *)
-  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
-				     if HI is in premisses, None otherwise *)
-  concl: types;            (* Qi x1...xni HI (f...), HI and (f...)
-			      are optional and mutually exclusive *)
-  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
-  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
+  params: Context.Rel.t;      (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  nparams: int;               (* number of parameters *)
+  predicates: Context.Rel.t;  (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  npredicates: int;           (* Number of predicates *)
+  branches: Context.Rel.t;    (* branchr,...,branch1 *)
+  nbranches: int;             (* Number of branches *)
+  args: Context.Rel.t;        (* (xni, Ti_ni) ... (x1, Ti_1) *)
+  nargs: int;                 (* number of arguments *)
+  indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni)
+                                               if HI is in premisses, None otherwise *)
+  concl: types;               (* Qi x1...xni HI (f...), HI and (f...)
+			         are optional and mutually exclusive *)
+  indarg_in_concl: bool;      (* true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;        (* true if (f...) appears at the end of conclusion *)
 }
 
 let empty_scheme =
@@ -3303,7 +3302,7 @@ let hyps_of_vars env sign nogen hyps =
   if Id.Set.is_empty hyps then []
   else
     let (_,lh) =
-      Context.fold_named_context_reverse
+      Context.Named.fold_inside
         (fun (hs,hl) (x,_,_ as d) ->
 	  if Id.Set.mem x nogen then (hs,hl)
 	  else if Id.Set.mem x hs then (hs,x::hl)
@@ -3534,7 +3533,7 @@ let occur_rel n c =
    We also return the conclusion.
 *)
 let decompose_paramspred_branch_args elimt =
-  let rec cut_noccur elimt acc2 : rel_context * rel_context * types =
+  let rec cut_noccur elimt acc2 : Context.Rel.t * Context.Rel.t * types =
     match kind_of_term elimt with
       | Prod(nme,tpe,elimt') ->
 	  let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in
@@ -3543,7 +3542,7 @@ let decompose_paramspred_branch_args elimt =
 	  else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
       | App(_, _) | Rel _ -> acc2 , [] , elimt
       | _ -> error_ind_scheme "" in
-  let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types =
+  let rec cut_occur elimt acc1 : Context.Rel.t * Context.Rel.t * Context.Rel.t * types =
     match kind_of_term elimt with
       | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1)
       | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
@@ -3671,7 +3670,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	    let ind_is_ok =
 	      List.equal Term.eq_constr
 		(List.lastn scheme.nargs indargs)
-		(extended_rel_list 0 scheme.args) in
+		(Context.Rel.to_extended_list 0 scheme.args) in
 	    if not (ccl_arg_ok && ind_is_ok) then
 	      error_ind_scheme "the conclusion of"
 	  in (cond, check_concl)
@@ -4586,10 +4585,10 @@ let abstract_subproof id gk tac =
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) ->
 	if mem_named_context id current_sign &&
-          interpretable_as_section_decl evdref (Context.lookup_named id current_sign) d
+          interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
         then (s1,push_named_context_val d s2)
-	else (add_named_decl d s1,s2))
-      global_sign (empty_named_context,empty_named_context_val) in
+	else (Context.Named.add d s1,s2))
+      global_sign (Context.Named.empty, empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
   let concl =
@@ -4617,7 +4616,7 @@ let abstract_subproof id gk tac =
   in
   let const, args =
     if !shrink_abstract then shrink_entry sign const
-    else (const, List.rev (instance_from_named_context sign))
+    else (const, List.rev (Context.Named.to_instance sign))
   in
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 098212048..2ae72f4a5 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -9,7 +9,6 @@
 open Loc
 open Names
 open Term
-open Context
 open Environ
 open Proof_type
 open Evd
@@ -33,9 +32,9 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
 val refine          : constr -> tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
+val convert_hyp     : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
 val thin            : Id.t list -> tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
@@ -50,7 +49,7 @@ val convert_leq     : constr -> constr -> unit Proofview.tactic
 
 val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
 val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
-val find_intro_names : rel_context -> goal sigma -> Id.t list
+val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
@@ -180,7 +179,7 @@ val revert        : Id.t list -> unit Proofview.tactic
 (** {6 Resolution tactics. } *)
 
 val apply_type : constr -> constr list -> unit Proofview.tactic
-val bring_hyps : named_context -> unit Proofview.tactic
+val bring_hyps : Context.Named.t -> unit Proofview.tactic
 
 val apply                 : constr -> unit Proofview.tactic
 val eapply                : constr -> unit Proofview.tactic
@@ -239,20 +238,20 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  params: rel_context;     (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
-  nparams: int;            (** number of parameters *)
-  predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
-  npredicates: int;        (** Number of predicates *)
-  branches: rel_context;   (** branchr,...,branch1 *)
-  nbranches: int;          (** Number of branches *)
-  args: rel_context;       (** (xni, Ti_ni) ... (x1, Ti_1) *)
-  nargs: int;              (** number of arguments *)
-  indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni)
-				     if HI is in premisses, None otherwise *)
-  concl: types;            (** Qi x1...xni HI (f...), HI and (f...)
-			      are optional and mutually exclusive *)
-  indarg_in_concl: bool;   (** true if HI appears at the end of conclusion *)
-  farg_in_concl: bool;     (** true if (f...) appears at the end of conclusion *)
+  params: Context.Rel.t;      (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  nparams: int;               (** number of parameters *)
+  predicates: Context.Rel.t;  (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  npredicates: int;           (** Number of predicates *)
+  branches: Context.Rel.t;    (** branchr,...,branch1 *)
+  nbranches: int;             (** Number of branches *)
+  args: Context.Rel.t;        (** (xni, Ti_ni) ... (x1, Ti_1) *)
+  nargs: int;                 (** number of arguments *)
+  indarg: Context.Rel.Declaration.t option;  (** Some (H,I prm1..prmp x1...xni)
+	  		 	                 if HI is in premisses, None otherwise *)
+  concl: types;               (** Qi x1...xni HI (f...), HI and (f...)
+			          are optional and mutually exclusive *)
+  indarg_in_concl: bool;      (** true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;        (** true if (f...) appears at the end of conclusion *)
 }
 
 val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme