Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7

32 files changed, 510 insertions, 229 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cfbd760d8..f0be35882 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -145,5 +145,6 @@ let cook_constant env r =
   let cb = lookup_constant r.d_from env in
   let typ = expmod_type env r.d_modlist cb.const_type in
   let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
-  let hyps = map_named_context (expmod_constr env r.d_modlist) cb.const_hyps in
+  let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
+  let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in
   abstract_constant r.d_abstract hyps (body,typ)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8be72eb94..9de1866cc 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -12,7 +12,7 @@ type constant_body = {
   const_kind : path_kind;
   const_body : constr option;
   const_type : types;
-  const_hyps : named_context;
+  const_hyps : section_context;
   const_constraints : constraints;
   mutable const_opaque : bool }
 
@@ -52,12 +52,13 @@ type one_inductive_body = {
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
-  mind_nparams : int }
+  mind_nparams : int;
+  mind_params_ctxt : rel_context }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
-  mind_hyps : named_context;
+  mind_hyps : section_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option }
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index aca660567..531a616ba 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -17,7 +17,7 @@ type constant_body = {
   const_kind : path_kind;
   const_body : constr option;
   const_type : types;
-  const_hyps : named_context; (* New: younger hyp at top *)
+  const_hyps : section_context; (* New: younger hyp at top *)
   const_constraints : constraints;
   mutable const_opaque : bool }
 
@@ -61,12 +61,13 @@ type one_inductive_body = {
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
-  mind_nparams : int }
+  mind_nparams : int;
+  mind_params_ctxt : rel_context }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
-  mind_hyps : named_context;
+  mind_hyps : section_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index cb4b1e003..6bec01ecd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -283,16 +283,28 @@ let name_assumption env (na,c,t) =
 let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b 
 let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
 
-let it_mkProd_or_LetIn_name   env = List.fold_left (mkProd_or_LetIn_name env)
-let it_mkLambda_or_LetIn_name env = List.fold_left (mkLambda_or_LetIn_name env)
+let name_context env hyps =
+  snd
+    (List.fold_left
+       (fun (env,hyps) d -> 
+	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+       (env,[]) (List.rev hyps))
 
 let it_mkProd_wo_LetIn   = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
 
+let it_mkProd_or_LetIn_name env b hyps =
+  it_mkProd_or_LetIn b (name_context env hyps)
+
+let it_mkLambda_or_LetIn_name env b hyps =
+  it_mkLambda_or_LetIn b (name_context env hyps)
+
 let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
 let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
 
+let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn
+
 let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 65a2bb671..eba1e0979 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -140,6 +140,7 @@ val it_mkProd_or_LetIn : constr -> rel_context -> constr
 
 val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 val it_mkNamedProd_or_LetIn : constr -> named_context -> constr
+val it_mkNamedProd_wo_LetIn : constr -> named_context -> constr
 
 (* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
    from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2307a405f..228e2bafa 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -132,16 +132,20 @@ let failwith_non_pos_vect n ntypes v =
   done;
   anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
 
-let check_correct_par env nparams ntypes n l largs =
+let check_correct_par env hyps nparams ntypes n l largs =
   let largs = Array.of_list largs in
   if Array.length largs < nparams then 
     raise (IllFormedInd (LocalNotEnoughArgs l));
   let (lpar,largs') = array_chop nparams largs in
-  for k = 0 to nparams - 1 do
-    match kind_of_term (whd_betadeltaiotaeta env Evd.empty lpar.(k)) with
-      | IsRel w when (n-k-1 = w) -> ()
-      | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
-  done;
+  let nhyps = List.length hyps in
+  let rec check k index = function
+    | [] -> ()
+    | (_,Some _,_)::hyps -> check k (index+1) hyps
+    | _::hyps ->
+        match kind_of_term (whd_betadeltaiotaeta env Evd.empty lpar.(k)) with
+	  | IsRel w when w = index -> check (k-1) (index+1) hyps
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+  in check (nparams-1) (n-nhyps) hyps;
   if not (array_for_all (noccur_between n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
 
@@ -156,7 +160,8 @@ let abstract_mind_lc env ntyps npars lc =
     in 
     Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc
 
-let listrec_mconstr env ntypes nparams i indlc =
+let listrec_mconstr env ntypes hyps nparams i indlc =
+  let nhyps = List.length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos env n c = 
     let x,largs = whd_betadeltaiota_stack env Evd.empty c in
@@ -168,10 +173,10 @@ let listrec_mconstr env ntypes nparams i indlc =
 	  check_pos (push_rel_assum (na, b) env) (n+1) d
       | IsRel k ->
           if k >= n && k<n+ntypes then begin
-	    check_correct_par env nparams ntypes n (k-n+1) largs;
+	    check_correct_par env hyps nparams ntypes n (k-n+1) largs;
 	    Mrec(n+ntypes-k-1)
           end else if List.for_all (noccur_between n ntypes) largs then 
-	    if (n-nparams) <= k & k <= (n-1) 
+	    if (n-nhyps) <= k & k <= (n-1) 
 	    then Param(n-1-k)
             else Norec
 	  else
@@ -200,7 +205,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
     let newidx = n + auxntyp in
 (* Extends the environment with a variable corresponding to the inductive def *)
-    let env' = push_rel_assum (Anonymous,mis_user_arity mispeci) env in
+    let env' = push_rel_assum (Anonymous,mis_arity mispeci) env in
     let _ = 
       (* fails if the inductive type occurs non positively *)
       (* when substituted *) 
@@ -270,7 +275,7 @@ let listrec_mconstr env ntypes nparams i indlc =
 	| hd ->
 	    if check_head then
 	      if hd = IsRel (n+ntypes-i) then
-		check_correct_par env nparams ntypes n (ntypes-i+1) largs
+		check_correct_par env hyps nparams ntypes n (ntypes-i+1) largs
 	      else
 		raise (IllFormedInd LocalNotConstructor)
 	    else
@@ -282,12 +287,12 @@ let listrec_mconstr env ntypes nparams i indlc =
   Array.map
     (fun c ->
        let c = body_of_type c in
-       let sign, rawc = mind_extract_params nparams c in
+       let sign, rawc = mind_extract_params nhyps c in
        let env' = push_rels sign env in
        try
-	 check_construct env' true (1+nparams) rawc
+	 check_construct env' true (1+nhyps) rawc
        with IllFormedInd err -> 
-	 explain_ind_err (ntypes-i+1) env nparams c err)
+	 explain_ind_err (ntypes-i+1) env nhyps c err)
     indlc
     
 let is_recursive listind =
@@ -299,10 +304,38 @@ let is_recursive listind =
   in 
   array_exists one_is_rec
 
-let cci_inductive env env_ar kind finite inds cst =
+let abstract_inductive ntypes hyps (par,np,id,arity,cnames,issmall,isunit,lc) =
+  let args = instance_from_named_context (List.rev hyps) in
+  let nhyps = List.length hyps in
+  let nparams = List.length args in (* nparams = nhyps - nb(letin) *)
+  let new_refs =
+    list_tabulate (fun k -> applist(mkRel (k+nhyps+1),args)) ntypes in
+  let abs_constructor b = it_mkNamedProd_or_LetIn (substl new_refs b) hyps in
+  let lc' = Array.map abs_constructor lc in
+  let arity' = it_mkNamedProd_or_LetIn arity hyps in
+  let par' = push_named_to_rel_context hyps par in
+  (par',np+nparams,id,arity',cnames,issmall,isunit,lc')
+
+let cci_inductive locals env env_ar kind finite inds cst =
   let ntypes = List.length inds in
-  let one_packet i (nparams,id,ar,cnames,issmall,isunit,lc) =
-    let recargs = listrec_mconstr env_ar ntypes nparams i lc in
+  let ids = 
+    List.fold_left 
+      (fun acc (_,_,_,ar,_,_,_,lc) -> 
+	 Idset.union (global_vars_set (body_of_type ar))
+	   (Array.fold_left
+	      (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
+	      acc
+	      lc))
+      Idset.empty inds
+  in
+  let hyps = keep_hyps ids (named_context env) in
+  let inds' =
+    if Options.immediate_discharge then
+      List.map (abstract_inductive ntypes hyps) inds
+    else
+      inds in
+  let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) =
+    let recargs = listrec_mconstr env_ar ntypes params nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
     let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
     
@@ -327,22 +360,14 @@ let cci_inductive env env_ar kind finite inds cst =
       mind_kelim = kelim;
       mind_listrec = recargs;
       mind_finite = finite;
-      mind_nparams = nparams }
-  in
-  let ids = 
-    List.fold_left 
-      (fun acc (_,_,ar,_,_,_,lc) -> 
-	 Idset.union (global_vars_set (body_of_type ar))
-	   (Array.fold_left
-	      (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
-	      acc
-	      lc))
-      Idset.empty inds
+      mind_nparams = nparams;
+      mind_params_ctxt = params }
   in
-  let packets = Array.of_list (list_map_i one_packet 1 inds) in
+  let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in
+  let packets = Array.of_list (list_map_i one_packet 1 inds') in
   { mind_kind = kind;
     mind_ntypes = ntypes;
-    mind_hyps = keep_hyps ids (named_context env);
+    mind_hyps = sp_hyps;
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index be97f5249..d0e3a4cb0 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -42,8 +42,9 @@ val mind_check_wellformed : env -> mutual_inductive_entry -> unit
 (* [cci_inductive] checks positivity and builds an inductive body *)
 
 val cci_inductive : 
-  env -> env -> path_kind -> bool -> 
-   (int * identifier * types * identifier list * bool * bool * types array)
+  (identifier * variable_path) list -> env -> env -> path_kind -> bool -> 
+   (Sign.rel_context * int * identifier * types * 
+    identifier list * bool * bool * types array)
       list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 493cb15f5..b444baa8d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -37,13 +37,16 @@ let mis_typename mis = mis.mis_mip.mind_typename
 let mis_typepath mis =
   make_path (dirpath mis.mis_sp) mis.mis_mip.mind_typename CCI
 let mis_consnames mis = mis.mis_mip.mind_consnames
+let mis_conspaths mis =
+  let dir = dirpath mis.mis_sp in
+  Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames
 let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
 let mis_finite mis = mis.mis_mip.mind_finite
 
 let mis_typed_nf_lc mis =
   let sign = mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in
-  Array.map (fun t -> Instantiate.instantiate_type sign t args)
+  Array.map (fun t -> (* Instantiate.instantiate_type sign*) t (*args*))
     mis.mis_mip.mind_nf_lc
 
 let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
@@ -51,25 +54,14 @@ let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
 let mis_user_lc mis = 
   let sign = mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in
-  Array.map (fun t -> Instantiate.instantiate_type sign t args)
+  Array.map (fun t -> (*Instantiate.instantiate_type sign*) t (*args*))
     (mind_user_lc mis.mis_mip)
 
 (* gives the vector of constructors and of 
    types of constructors of an inductive definition 
    correctly instanciated *)
 
-let mis_type_mconstructs mispec =
-  let specif = Array.map body_of_type (mis_user_lc mispec)
-  and ntypes = mis_ntypes mispec
-  and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) 
-  and make_Ck k = mkMutConstruct
-		    (((mispec.mis_sp,mispec.mis_tyi),k+1),
-		       mispec.mis_args) in
-  (Array.init nconstr make_Ck, 
-   Array.map (substl (list_tabulate make_Ik ntypes)) specif)
-
-let mis_type_nf_mconstruct i mispec =
+let mis_nf_constructor_type i mispec =
   let specif = mis_nf_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
@@ -77,15 +69,15 @@ let mis_type_nf_mconstruct i mispec =
   if i > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
-let mis_type_mconstruct i mispec = 
+let mis_constructor_type i mispec = 
   let specif = mis_user_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
   let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
-  type_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
+  substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
-let mis_user_arity mis =
+let mis_arity mis =
   let hyps = mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in
   Instantiate.instantiate_type hyps (mind_user_arity mis.mis_mip) largs
@@ -95,11 +87,13 @@ let mis_nf_arity mis =
   and largs = Array.to_list mis.mis_args in
   Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
 
-let mis_params_ctxt mispec =
+let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
+(*
   let paramsign,_ =
-    decompose_prod_n_assum mispec.mis_mip.mind_nparams
-      (body_of_type (mis_nf_arity mispec))
+    decompose_prod_n_assum mis.mis_mip.mind_nparams
+      (body_of_type (mis_nf_arity mis))
   in paramsign
+*)
 
 let mis_sort mispec = mispec.mis_mip.mind_sort
 
@@ -239,10 +233,33 @@ let lift_constructor n cs = {
   cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
 }
 
-let get_constructor (IndFamily (mispec,params)) j =
+let instantiate_params t args sign =
+  let rec inst s t = function
+    | ((_,None,_)::ctxt,a::args) ->
+	(match kind_of_term t with
+	   | IsProd(_,_,t) -> inst (a::s) t (ctxt,args)
+	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+    | ((_,(Some b),_)::ctxt,args) -> 
+	(match kind_of_term t with
+	   | IsLetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
+	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+    | [], [] -> substl s t
+    | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
+  in inst [] t (List.rev sign,args)
+
+let get_constructor_type (IndFamily (mispec,params)) j =
   assert (j <= mis_nconstr mispec);
-  let typi = mis_type_nf_mconstruct j mispec in
-  let (args,ccl) = decompose_prod_assum (prod_applist typi params) in
+  let typi = mis_constructor_type j mispec in
+  instantiate_params typi params (mis_params_ctxt mispec)
+
+let get_constructors_types (IndFamily (mispec,params) as indf) =
+  Array.init (mis_nconstr mispec) (fun j -> get_constructor_type indf (j+1))
+
+let get_constructor (IndFamily (mispec,params) as indf) j =
+  assert (j <= mis_nconstr mispec);
+  let typi = mis_nf_constructor_type j mispec in
+  let typi = instantiate_params typi params (mis_params_ctxt mispec) in
+  let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = whd_stack ccl in
   let (_,vargs) = list_chop (mis_nparams mispec) allargs in
   { cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) j;
@@ -254,8 +271,14 @@ let get_constructor (IndFamily (mispec,params)) j =
 let get_constructors (IndFamily (mispec,params) as indf) =
   Array.init (mis_nconstr mispec) (fun j -> get_constructor indf (j+1))
 
+let get_arity_type (IndFamily (mispec,params)) =
+  let arity = body_of_type (mis_arity mispec) in
+(*  instantiate_params arity params (mis_params_ctxt mispec) *)
+  prod_applist arity params
+
 let get_arity (IndFamily (mispec,params)) =
   let arity = body_of_type (mis_nf_arity mispec) in
+(*  instantiate_params arity params (mis_params_ctxt mispec) *)
   destArity (prod_applist arity params)
 
 (* Functions to build standard types related to inductive *)
@@ -299,3 +322,23 @@ let build_branch_type env dep p cs =
       cs.cs_args
   else
     it_mkProd_or_LetIn base cs.cs_args
+
+(* [Rel (n+m);...;Rel(n+1)] *)
+
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+  in 
+  reln [] 1
+
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
+  in 
+  reln [] 1 hyps
+
+let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 47d98e608..e7504bf16 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -42,17 +42,16 @@ val mis_typepath : inductive_instance -> section_path
 val mis_is_recursive_subset : int list -> inductive_instance -> bool
 val mis_is_recursive : inductive_instance -> bool
 val mis_consnames : inductive_instance -> identifier array
+val mis_conspaths : inductive_instance -> section_path array
 val mis_inductive : inductive_instance -> inductive
-val mis_nf_arity : inductive_instance -> types
-val mis_user_arity : inductive_instance -> types
+val mis_arity : inductive_instance -> types
 val mis_params_ctxt : inductive_instance -> rel_context
 val mis_sort : inductive_instance -> sorts
-val mis_type_mconstruct : int -> inductive_instance -> types
+val mis_constructor_type : int -> inductive_instance -> types
 val mis_finite : inductive_instance -> bool 
 
 (* The ccl of constructor is pre-normalised in the following functions *)
 val mis_nf_lc : inductive_instance -> constr array
-val mis_type_mconstructs : inductive_instance -> constr array * constr array
 
 (*s [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = IndFamily of inductive_instance * constr list
@@ -117,6 +116,16 @@ val build_dependent_constructor : constructor_summary -> constr
    the constructor argument of a dependent predicate in a cases branch *)
 val build_dependent_inductive : inductive_family -> constr
 
+(*s [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
+(* (this is iota operator in C. Paulin habilitation thesis) *)
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
+
+(*s [extended_rel_vect n hyps] and [extended_rel_list n hyps]
+    generalizes [rel_vect] when local definitions may occur in parameters *)
+val extended_rel_vect : int -> rel_context -> constr array
+val extended_rel_list : int -> rel_context -> constr list
+
 (* if the arity for some inductive family [indf] associated to [(I
    params)] is [(x1:A1)...(xn:An)sort'] then [make_arity env sigma dep
    indf k] builds [(x1:A1)...(xn:An)sort] which is the arity of an
@@ -157,6 +166,14 @@ val lookup_mind_specif : inductive -> env -> inductive_instance
 
 val find_rectype : env -> 'a evar_map -> constr -> inductive_type
 
+(* [get_constructors_types indf] returns the array of the types of
+   constructors of the inductive\_family [indf], i.e. the types are
+   instantiated by the parameters of the family (the type may be not
+   in canonical form -- e.g. cf sets library) *)
+
+val get_constructors_types : inductive_family -> types array
+val get_constructor_type : inductive_family -> int -> types
+
 (* [get_constructors indf] build an array of [constructor_summary]
    from some inductive type already analysed as an [inductive_family];
    global parameters are already instanciated in the constructor
@@ -165,17 +182,24 @@ val find_rectype : env -> 'a evar_map -> constr -> inductive_type
    are not renamed when [Anonymous] *)
 
 val get_constructors : inductive_family -> constructor_summary array
-
 val get_constructor : inductive_family -> int -> constructor_summary
 
-(* [get_arity indf] returns the product and the sort of the arity of
-   the inductive family described by [indf]; global parameters are
-   already instanciated; the products signature is relative to the
+(* [get_arity_type indf] returns the type of the arity of the
+   inductive family described by [indf]; global parameters are already
+   instanciated (but the type may be not in canonical form -- e.g. cf
+   sets library); the products signature is relative to the
    environment definition of [indf]; the names of the products of the
-   constructors types are not renamed when [Anonymous] *)
+   constructors types are not renamed when [Anonymous]; [get_arity
+   indf] does the same but normalises and decomposes it as an arity *)
 
+val get_arity_type : inductive_family -> types
 val get_arity : inductive_family -> arity
 
+(* [get_arity_type indf] returns the type of the arity of the inductive
+   family described by [indf]; global parameters are already instanciated *)
+
+
+
 (* Examples: assume
   
 \begin{verbatim}
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index c9e39c9f5..27754ae84 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -17,13 +17,22 @@ let is_id_inst inst =
   in
   List.for_all is_id inst
 
-let instantiate_constr sign c args =
+let instantiate sign c args =
   let inst = instantiate_named_context sign args in
   if is_id_inst inst then
     c
   else
     replace_vars inst c
 
+let instantiate_evar = instantiate
+
+let instantiate_constr sign c args =
+  if Options.immediate_discharge then
+    c
+  else
+    let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
+    instantiate sign c args
+
 let instantiate_type sign tty args =
   type_app (fun c -> instantiate_constr sign c args) tty
 
@@ -33,7 +42,7 @@ let instantiate_type sign tty args =
 let constant_type env sigma (sp,args) =
   let cb = lookup_constant sp env in
   (* TODO: check args *)
-  instantiate_type cb.const_hyps cb.const_type (Array.to_list args)
+(*  instantiate_type cb.const_hyps *) cb.const_type (*(Array.to_list args)*)
 
 type const_evaluation_result = NoBody | Opaque
 
@@ -60,7 +69,7 @@ let existential_type sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = info.evar_hyps in
   (* TODO: check args [this comment was in Typeops] *)
-  instantiate_constr hyps info.evar_concl (Array.to_list args)
+  instantiate_evar hyps info.evar_concl (Array.to_list args)
 
 exception NotInstantiatedEvar
 
@@ -69,7 +78,7 @@ let existential_value sigma (n,args) =
   let hyps = info.evar_hyps in
   match evar_body info with
     | Evar_defined c ->
-	instantiate_constr hyps c (Array.to_list args)
+	instantiate_evar hyps c (Array.to_list args)
     | Evar_empty ->
 	raise NotInstantiatedEvar
 
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index a80dcc435..1414196f3 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -12,9 +12,9 @@ open Environ
 (* Instantiation of constants and inductives on their real arguments. *)
 
 val instantiate_constr : 
-  named_context -> constr -> constr list -> constr
+  section_context -> constr -> constr list -> constr
 val instantiate_type : 
-  named_context -> types -> constr list -> types
+  section_context -> types -> constr list -> types
 
 (*s [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
diff --git a/kernel/names.ml b/kernel/names.ml
index 8b1cb71a1..fc3453611 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -235,6 +235,10 @@ let next_name_away name l =
     | Name str  -> next_ident_away str l
     | Anonymous -> id_of_string "_"
 
+let out_name = function
+  | Name id -> id
+  | Anonymous -> anomaly "out_name: expects a defined name"
+
 (* Kinds *)
 
 type path_kind = CCI | FW | OBJ
diff --git a/kernel/names.mli b/kernel/names.mli
index bd3d0e590..edcadf634 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -41,6 +41,9 @@ val next_name_away : name -> identifier list -> identifier
 val next_name_away_with_default : 
   string -> name -> identifier list -> identifier
 
+(* [out_name na] raises an anomaly if [na] is [Anonymous] *)
+val out_name : name -> identifier
+
 (*s [path_kind] is currently degenerated, [FW] is not used *)
 type path_kind = CCI | FW | OBJ
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 600cdd823..794c49354 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -59,16 +59,19 @@ val nf_betadeltaiota : 'a reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betadeltaiota : 'a contextual_reduction_function
+val whd_betadeltaiota_nolet : 'a contextual_reduction_function
 val whd_betaetalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
 val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack : 'a contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betadeltaiota_state : 'a contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state : 'a contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
 
 (*s Head normal forms *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 925ca9bf0..72e9bfd1a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -297,36 +297,49 @@ let safe_infer_declaration env = function
       let (j,cst) = safe_infer env t in
       None, assumption_of_judgment env Evd.empty j, cst
 
-let add_global_declaration sp env (body,typ,cst) =
+type local_names = (identifier * variable_path) list
+
+let add_global_declaration sp env locals (body,typ,cst) =
   let env' = add_constraints cst env in
   let ids = match body with 
     | None -> global_vars_set typ
     | Some b -> Idset.union (global_vars_set b) (global_vars_set typ) in
+  let hyps = keep_hyps ids (named_context env) in
+  let body, typ =
+    if Options.immediate_discharge then
+      option_app (fun c -> it_mkNamedLambda_or_LetIn c hyps) body,
+      it_mkNamedProd_or_LetIn typ hyps
+    else
+      body,typ in
+  let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals, b, t)) hyps in
   let cb = {
     const_kind = kind_of_path sp;
     const_body = body;
     const_type = typ;
-    const_hyps = keep_hyps ids (named_context env);
+    const_hyps = sp_hyps;
     const_constraints = cst;
     const_opaque = false } 
   in
   Environ.add_constant sp cb env'
 
-let add_parameter sp t env =
-  add_global_declaration sp env (safe_infer_declaration env (Assum t))
+let add_parameter sp t locals env =
+  add_global_declaration sp env locals (safe_infer_declaration env (Assum t))
 
-let add_constant_with_value sp body typ env =
+let add_constant_with_value sp body typ locals env =
   let body' =
     match typ with
       | None -> body
       | Some ty -> mkCast (body, ty) in
-  add_global_declaration sp env (safe_infer_declaration env (Def body'))
+  add_global_declaration sp env locals (safe_infer_declaration env (Def body'))
+
+let add_constant sp ce locals env =
+  add_constant_with_value sp ce.const_entry_body ce.const_entry_type locals env
 
-let add_discharged_constant sp r env =
+let add_discharged_constant sp r locals env =
   let (body,typ) = Cooking.cook_constant env r in
   match body with
     | None -> 
-	add_parameter sp typ env
+	add_parameter sp typ [] (* Bricolage avant poubelle *) env
     | Some c -> 
 	(* let c = hcons1_constr c in *)
 	let (jtyp,cst) = safe_infer env typ in
@@ -335,17 +348,19 @@ let add_discharged_constant sp r env =
 	  Idset.union (global_vars_set c) 
 	    (global_vars_set (body_of_type jtyp.uj_val))
 	in
-	let cb = { const_kind = kind_of_path sp;
-		   const_body = Some c;
-		   const_type = assumption_of_judgment env' Evd.empty jtyp;
-		   const_hyps = keep_hyps ids (named_context env);
-		   const_constraints = cst;
-		   const_opaque = false } 
+	let hyps = keep_hyps ids (named_context env) in
+	let sp_hyps =
+	  List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in
+	let cb =
+	  { const_kind = kind_of_path sp;
+	    const_body = Some c;
+	    const_type = assumption_of_judgment env' Evd.empty jtyp;
+	    const_hyps = sp_hyps;
+	    const_constraints = cst;
+	    const_opaque = false } 
 	in
-	add_constant sp cb env'
+	Environ.add_constant sp cb env'
 
-let add_constant sp ce env =
-  add_constant_with_value sp ce.const_entry_body ce.const_entry_type env
 
 (* Insertion of inductive types. *)
 
@@ -427,7 +442,7 @@ let infer_constructor_packet env_ar params short_arity arsort vc =
   let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
   (issmall,isunit,vc', cst)
 
-let add_mind sp mie env =
+let add_mind sp mie locals env =
   mind_check_wellformed env mie;
 
   (* We first type params and arity of each inductive definition *)
@@ -466,7 +481,8 @@ let add_mind sp mie env =
 	 in
 	 let nparams = ind.mind_entry_nparams in
 	 let consnames = ind.mind_entry_consnames in
-	 let ind' = (nparams,id,full_arity,consnames,issmall,isunit,lc') in
+	 let ind' = (params,nparams,id,full_arity,consnames,issmall,isunit,lc')
+	 in
 	 (ind'::inds, Constraint.union cst cst'))
       mie.mind_entry_inds
       params_arity_list
@@ -474,7 +490,7 @@ let add_mind sp mie env =
 
   (* Finally, we build the inductive packet and push it to env *)
   let kind = kind_of_path sp in
-  let mib = cci_inductive env env_arities kind mie.mind_entry_finite inds cst
+  let mib = cci_inductive locals env env_arities kind mie.mind_entry_finite inds cst
   in
   add_mind sp mib (add_constraints cst env)
     
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7f50c7104..474da34b8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -31,15 +31,18 @@ val push_named_assum :
 val push_named_def :
   identifier * constr -> safe_environment -> safe_environment
 
+type local_names = (identifier * variable_path) list
+
 val add_parameter :
-  section_path -> constr -> safe_environment -> safe_environment
+  section_path -> constr -> local_names -> safe_environment -> safe_environment
 val add_constant : 
-  section_path -> constant_entry -> safe_environment -> safe_environment
+  section_path -> constant_entry -> local_names -> 
+    safe_environment -> safe_environment
 val add_discharged_constant : 
-  section_path -> Cooking.recipe -> safe_environment -> safe_environment
+  section_path -> Cooking.recipe -> local_names -> safe_environment -> safe_environment
 
 val add_mind : 
-  section_path -> mutual_inductive_entry -> safe_environment 
+  section_path -> mutual_inductive_entry -> local_names -> safe_environment 
     -> safe_environment
 val add_constraints : constraints -> safe_environment -> safe_environment
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index efdc08a3f..fc3e15f5e 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -50,8 +50,24 @@ let fold_named_context_reverse = List.fold_left
 let fold_named_context_both_sides = list_fold_right_and_left
 let it_named_context_quantifier f = List.fold_left (fun c d -> f d c)
 
+(*s Signatures of ordered section variables *)
+
+type section_declaration = variable_path * constr option * constr
+type section_context = section_declaration list
+let rec instance_from_section_context = function
+  | (sp,None,_) :: sign -> 
+      mkVar (basename sp) :: instance_from_section_context sign
+  | _ :: sign -> instance_from_section_context sign
+  | [] -> []
+let instance_from_section_context x =
+  if Options.immediate_discharge then [] else instance_from_section_context x
+
+(*s Signatures of ordered optionally named variables, intended to be
+   accessed by de Bruijn indices *)
+
 type rel_declaration = name * constr option * types
 type rel_context = rel_declaration list
+type rev_rel_context = rel_declaration list
 
 let add_rel_decl = add
 let add_rel_assum = add_decl
@@ -87,6 +103,14 @@ let lift_rel_context n sign =
     | [] -> []
   in
   liftrec (rel_context_length sign) sign
+let lift_rev_rel_context n sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,option_app (liftn n k) c,type_app (liftn n k) t)
+	::(liftrec (k+1) sign)
+    | [] -> []
+  in
+  liftrec 1 sign
 let concat_rel_context = (@)
 let ids_of_rel_context sign =
   List.fold_right
@@ -98,6 +122,22 @@ let assums_of_rel_context sign =
     (fun (na,c,t) l -> match c with Some _ -> l | None -> (na,body_of_type t)::l)
     sign []
 let map_rel_context = map
+let push_named_to_rel_context hyps ctxt =
+  let rec push = function
+    | (id,b,t) :: l ->
+	let s, hyps = push l in
+	let d = (Name id, option_app (subst_vars s) b, subst_vars s t) in
+	id::s, d::hyps
+    | [] -> [],[] in
+  let s, hyps = push hyps in
+  let rec subst = function
+    | (na,b,t) :: l ->
+	let n, ctxt = subst l in
+	let d = (na, option_app (substn_vars n s) b, substn_vars n s t) in
+	(n+1), d::ctxt
+    | [] -> 1, hyps in
+  snd (subst ctxt)
+let reverse_rel_context = List.rev
 
 let instantiate_sign sign args =
   let rec instrec = function
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 5c93bccbf..ede431eb4 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -36,11 +36,22 @@ val instantiate_sign :
 val keep_hyps : Idset.t -> named_context -> named_context
 val instance_from_named_context : named_context -> constr list
 
+(*s Signatures of ordered section variables *)
+
+type section_declaration = variable_path * constr option * constr
+type section_context = section_declaration list
+
+val instance_from_section_context : section_context -> constr list
+
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
 
+(* In [rel_context], more recent declaration is on top *)
 type rel_context = rel_declaration list
 
+(* In [rev_rel_context], older declaration is on top *)
+type rev_rel_context = rel_declaration list
+
 val add_rel_decl : (name * constr option * types) -> rel_context -> rel_context
 val add_rel_assum : (name * types) -> rel_context -> rel_context
 val add_rel_def : (name * constr * types) -> rel_context -> rel_context
@@ -50,10 +61,13 @@ val lookup_rel_id : identifier -> rel_context -> int * types
 val empty_rel_context : rel_context
 val rel_context_length : rel_context -> int
 val lift_rel_context : int -> rel_context -> rel_context
+val lift_rev_rel_context : int -> rev_rel_context -> rev_rel_context
 val concat_rel_context : newer:rel_context -> older:rel_context -> rel_context
 val ids_of_rel_context : rel_context -> identifier list
 val assums_of_rel_context : rel_context -> (name * constr) list
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+val push_named_to_rel_context : named_context -> rel_context -> rel_context
+val reverse_rel_context : rel_context -> rev_rel_context
 
 (*s This is used to translate names into de Bruijn indices and
    vice-versa without to care about typing information *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 7503aa03a..f942fe178 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -977,11 +977,13 @@ let replace_vars var_alist =
 let subst_var str = replace_vars [(str, mkRel 1)]
 
 (* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
-let subst_vars vars =
+let substn_vars p vars =
   let _,subst =
-    List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (1,[]) vars
+    List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (p,[]) vars
   in replace_vars (List.rev subst)
 
+let subst_vars = substn_vars 1
+
 (*********************)
 (* Term constructors *)
 (*********************)
@@ -1242,7 +1244,7 @@ let destArity =
     | IsLetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
     | IsCast (c,_)   -> prodec_rec l c
     | IsSort s       -> l,s
-    | _              -> anomaly "decompose_arity: not an arity"
+    | _              -> anomaly "destArity: not an arity"
   in 
   prodec_rec [] 
 
@@ -1387,16 +1389,6 @@ let global_vars_set constr =
   in 
   filtrec Idset.empty constr
 
-(* [Rel (n+m);...;Rel(n+1)] *)
-
-let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (mkRel(n+p)::l) (p+1)
-  in 
-  reln [] 1
-
 (* Rem: end of import from old module Generic *)
 
 (* Various occurs checks *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 08b1e5e86..858ba2465 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -474,9 +474,9 @@ val subst_var : identifier -> constr -> constr
    if two names are identical, the one of least indice is keeped *)
 val subst_vars : identifier list -> constr -> constr
 
-(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
-val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> constr list
+(* [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+   if two names are identical, the one of least indice is keeped *)
+val substn_vars : int -> identifier list -> constr -> constr
 
 (*s Compact representation of implicit lifts. \\
    [ELSHFT(l,n)] == lift of [n], then apply [lift l].
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index ae1bb46cf..fa3db0b86 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -78,21 +78,16 @@ let type_of_constant = Instantiate.constant_type
 
 (* Inductive types. *)
 
-let instantiate_arity = mis_user_arity
-
 let type_of_inductive env sigma i =
   (* TODO: check args *)
-  instantiate_arity (lookup_mind_specif i env)
+  mis_arity (lookup_mind_specif i env)
 
 (* Constructors. *)
 
-let type_mconstruct env sigma i mind =
-  mis_type_mconstruct i (lookup_mind_specif mind env)
-
 let type_of_constructor env sigma cstr =
-  type_mconstruct env sigma
-    (index_of_constructor cstr)
-    (inductive_of_constructor cstr)
+  mis_constructor_type
+    (index_of_constructor cstr) 
+    (lookup_mind_specif (inductive_of_constructor cstr) env)
 
 let type_of_existential env sigma ev =
   Instantiate.existential_type sigma ev
diff --git a/library/declare.ml b/library/declare.ml
index 82966022b..57e58256e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -48,12 +48,17 @@ type sticky = bool
 
 type variable_declaration = section_variable_entry * strength * sticky
 
-let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
+let vartab =
+  ref ((Spmap.empty, []) :
+       (identifier * variable_declaration) Spmap.t * section_path list)
+
+let current_section_context () =
+  List.map (fun sp -> (basename sp, sp)) (snd !vartab)
 
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
-	    Summary.init_function = (fun () -> vartab := Spmap.empty);
+	    Summary.init_function = (fun () -> vartab := (Spmap.empty, []));
 	    Summary.survive_section = false }
 
 let cache_variable (sp,(id,(d,_,_) as vd)) =
@@ -65,7 +70,7 @@ let cache_variable (sp,(id,(d,_,_) as vd)) =
     | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
   Nametab.push_local sp (VarRef sp);
-  vartab := Spmap.add sp vd !vartab
+  vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l)
 
 let (in_variable, out_variable) =
   let od = {
@@ -87,7 +92,7 @@ let cache_parameter (sp,c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_parameter"
       [< pr_id (basename sp); 'sTR " already exists" >];
-  Global.add_parameter sp c;
+  Global.add_parameter sp c (current_section_context ());
   Nametab.push sp (ConstRef sp)
 
 let load_parameter _ = ()
@@ -132,9 +137,10 @@ let cache_constant (sp,(cdt,stre,op)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
+  let sc = current_section_context() in
   begin match cdt with 
-    | ConstantEntry ce -> Global.add_constant sp ce
-    | ConstantRecipe r -> Global.add_discharged_constant sp r
+    | ConstantEntry ce -> Global.add_constant sp ce sc
+    | ConstantRecipe r -> Global.add_discharged_constant sp r sc
   end;
   Nametab.push sp (ConstRef sp);
   if op then Global.set_opaque sp;
@@ -197,7 +203,7 @@ let check_exists_inductive (sp,_) =
 let cache_inductive (sp,mie) =
   let names = inductive_names sp mie in
   List.iter check_exists_inductive names;
-  Global.add_mind sp mie;
+  Global.add_mind sp mie (current_section_context ());
   List.iter (fun (sp, ref) -> Nametab.push sp ref) names
 
 let load_inductive _ = ()
@@ -236,12 +242,12 @@ let constant_or_parameter_strength sp =
   try constant_strength sp with Not_found -> NeverDischarge
 
 let get_variable sp = 
-  let (id,(_,str,sticky)) = Spmap.find sp !vartab in
+  let (id,(_,str,sticky)) = Spmap.find sp (fst !vartab) in
   let (c,ty) = Global.lookup_named id in
   ((id,c,ty),str,sticky)
 
 let variable_strength sp =
-  let _,(_,str,_) = Spmap.find sp !vartab in str
+  let _,(_,str,_) = Spmap.find sp (fst !vartab) in str
 
 (* Global references. *)
 
@@ -267,11 +273,11 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let context_of_global_reference env = function
-  | VarRef sp -> [] (* Hum !, pas correct *)
-  | ConstRef sp -> (Environ.lookup_constant sp env).const_hyps
-  | IndRef (sp,_) -> (Environ.lookup_mind sp env).mind_hyps
-  | ConstructRef ((sp,_),_) -> (Environ.lookup_mind sp env).mind_hyps
+let context_of_global_reference = function
+  | VarRef sp -> []
+  | ConstRef sp -> (Global.lookup_constant sp).const_hyps
+  | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
+  | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
 
 (*
 let global_sp_operator env sp id =
@@ -282,87 +288,102 @@ let global_sp_operator env sp id =
     mind_oper_of_id sp id mib, mib.mind_hyps
 *)
 
-let occur_decl env (id,c,t) hyps =
-  try
-    let (c',t') = Sign.lookup_id id hyps in
-    let matching_bodies = match c,c' with
-      | None, _ -> true
-      | Some c, None -> false
-      | Some c, Some c' -> is_conv env Evd.empty c c' in
-    let matching_types = 
-      is_conv env Evd.empty (body_of_type t) (body_of_type t') in
-    matching_types & matching_bodies
-  with Not_found -> false
-
-(*
-let find_common_hyps_then_abstract c env hyps' hyps = 
-  snd (fold_named_context_both_sides
-	 (fun
-	    (env,c) (id,_,_ as d) hyps ->
-	      if occur_decl env d hyps' then 
-		(Environ.push_named_decl d env,c)
-	      else
-		let hyps'' = List.rev (d :: hyps) in
-		(env, Environ.it_mkNamedLambda_or_LetIn c hyps''))
-	 hyps
-	 (env,c))
-*)
+let rec occur_section_variable sp = function
+  | (_,sp')::_ when sp = sp' -> true
+  | _::l -> occur_section_variable sp l
+  | [] -> false
 
 let rec quantify_extra_hyps c = function
-  | (id,None,t)::hyps -> mkNamedLambda id t (quantify_extra_hyps c hyps)
+  | (sp,None,t)::hyps ->
+      mkNamedLambda (basename sp) t (quantify_extra_hyps c hyps)
   (* Buggé car id n'apparaît pas dans les instances des constantes dans c *)
   (* et id n'est donc pas substitué dans ces constantes *)
-  | (id,Some b,t)::hyps -> mkNamedLetIn id b t (quantify_extra_hyps c hyps)
+  | (sp,Some b,t)::hyps ->
+      mkNamedLetIn (basename sp) b t (quantify_extra_hyps c hyps)
   | [] -> c
 
-let rec find_common_hyps_then_abstract c env hyps' = function
-  | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
-      find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps
-  | hyps -> quantify_extra_hyps c hyps
+let find_common_hyps_then_abstract c hyps' hyps =
+  let rec find = function
+    | (sp,_,_) :: hyps when occur_section_variable sp hyps' -> find hyps
+    | hyps -> quantify_extra_hyps c hyps in
+  find (List.rev hyps)
 
-let find_common_hyps_then_abstract c env hyps' hyps =
-  find_common_hyps_then_abstract c env hyps' (List.rev hyps)
-
-let current_section_context () =
-  let current = Spmap.fold (fun _ (id,_) hyps -> id::hyps) !vartab [] in
-  List.fold_right
-    (fun (id,_,_ as d) hyps -> if List.mem id current then d::hyps else hyps)
-    (Global.named_context ()) []
+let section_variable_paths () = snd !vartab
 
 let find_section_variable id =
   let l =
     Spmap.fold
       (fun sp (id',_) hyps -> if id=id' then sp::hyps else hyps)
-      !vartab [] in
+      (fst !vartab) [] in
   match l with
     | [] -> raise Not_found
     | [sp] -> sp
     | _ -> error "Arghh, you blasted me with several variables of same name"
 
+let last_section_hyps dir =
+  List.fold_right
+    (fun sp hyps -> if dirpath sp = dir then basename sp :: hyps else hyps)
+    (snd !vartab) []
+
+let rec find_var id = function
+  | [] -> raise Not_found
+  | sp::l -> if basename sp = id then sp else find_var id l
+
+let implicit_section_args ref =
+  if Options.immediate_discharge then
+    let hyps = context_of_global_reference ref in
+    let hyps0 = section_variable_paths () in
+    let rec keep acc = function
+      | (sp,None,_)::hyps ->
+	  let acc = if List.mem sp hyps0 then sp::acc else acc in
+	  keep acc hyps
+      | (_,Some _,_)::hyps -> keep acc hyps
+      | [] -> acc
+    in keep [] hyps
+  else []
+
+let section_hyps ref =
+  let hyps = context_of_global_reference ref in
+  let hyps0 = section_variable_paths () in
+  let rec keep acc = function
+    | (sp,b,_ as d)::hyps ->
+	let acc = if List.mem sp hyps0 then (sp,b=None)::acc else acc in
+	keep acc hyps
+    | [] -> acc
+  in keep [] hyps
+
 let extract_instance ref args =
-  let hyps = context_of_global_reference (Global.env ()) ref in
+  if Options.immediate_discharge then args
+  else
+  let hyps = context_of_global_reference ref in
   let hyps0 = current_section_context () in
   let na = Array.length args in
   let rec peel n acc = function
-    | (_,None,_ as d)::hyps ->
-	if List.mem d hyps0 then peel (n-1) acc hyps
+    | (sp,None,_ as d)::hyps ->
+	if List.mem_assoc (basename sp) hyps0 then peel (n-1) acc hyps
 	else peel (n-1) (args.(n)::acc) hyps
     | (_,Some _,_)::hyps -> peel n acc hyps
     | [] -> Array.of_list acc
   in peel (na-1) [] hyps
 
-let constr_of_reference _ env ref =
-  let hyps = context_of_global_reference env ref in
+let constr_of_reference _ _ ref =
+if Options.immediate_discharge then
+  match ref with
+    | VarRef sp -> mkVar (basename sp)
+    | ConstRef sp -> mkConst (sp,[||])
+    | ConstructRef sp -> mkMutConstruct (sp,[||])
+    | IndRef sp -> mkMutInd (sp,[||])
+else
+  let hyps = context_of_global_reference ref in
   let hyps0 = current_section_context () in
-  let env0 = Environ.reset_context env in
-  let args = instance_from_named_context hyps in
+  let args = instance_from_section_context hyps in
   let body = match ref with
     | VarRef sp -> mkVar (basename sp)
     | ConstRef sp -> mkConst (sp,Array.of_list args)
     | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args)
     | IndRef sp -> mkMutInd (sp,Array.of_list args)
   in
-  find_common_hyps_then_abstract body env0 hyps0 hyps
+  find_common_hyps_then_abstract body hyps0 hyps
 
 let construct_absolute_reference env sp =
   constr_of_reference Evd.empty env (Nametab.absolute_reference sp)
@@ -384,6 +405,10 @@ let global_qualified_reference qid =
 let global_absolute_reference sp = 
   construct_absolute_reference (Global.env()) sp
 
+let global_reference_in_absolute_module dir id = 
+  constr_of_reference Evd.empty (Global.env())
+    (Nametab.locate_in_absolute_module dir id)
+
 let global_reference kind id = 
   construct_reference (Global.env()) kind id
 
@@ -414,6 +439,21 @@ let path_of_inductive_path (sp,tyi) =
     let (pa,_,k) = repr_path sp in 
     Names.make_path pa (mip.mind_typename) k 
 
+(* Util *)
+let instantiate_inductive_section_params t ind =
+  if Options.immediate_discharge then 
+  let sign = section_hyps (IndRef ind) in
+  let rec inst s ctxt t =
+    let k = kind_of_term t in
+    match (ctxt,k) with
+    | (sp,true)::ctxt, IsLambda(_,_,t) ->
+	inst ((mkVar (basename sp))::s) ctxt t
+    | (sp,false)::ctxt, IsLetIn(_,_,_,t) -> 
+	inst ((mkVar (basename sp))::s) ctxt t
+    | [], _ -> substl s t
+    | _ -> anomaly"instantiate_params: term and ctxt mismatch"
+  in inst [] sign t
+  else t
 (* Eliminations. *)
 
 let eliminations = [ (prop,"_ind") ; (spec,"_rec") ; (types,"_rect") ]
@@ -426,6 +466,9 @@ let elimination_suffix = function
 let declare_one_elimination mispec =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
+    (* Hack to get const_hyps right in the declaration *)
+    let c = instantiate_inductive_section_params c (fst (mis_inductive mispec))
+    in
     let _ = declare_constant (id_of_string na)
       (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
        NeverDischarge,false) in
@@ -444,10 +487,12 @@ let declare_one_elimination mispec =
 
 let declare_eliminations sp =
   let mib = Global.lookup_mind sp in
+(*
   let ids = ids_of_named_context mib.mind_hyps in
   if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then    error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
-  let ctxt = instance_from_named_context mib.mind_hyps in
+*)
+  let ctxt = instance_from_section_context mib.mind_hyps in
   for i = 0 to Array.length mib.mind_packets - 1 do
     if mind_type_finite mib i then
       let mispec = Global.lookup_mind_specif ((sp,i), Array.of_list ctxt) in 
diff --git a/library/declare.mli b/library/declare.mli
index 894cebd0d..07dc96914 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -72,6 +72,7 @@ val out_variable : Libobject.obj -> identifier * variable_declaration
 val get_variable : variable_path -> named_declaration * strength * sticky
 val variable_strength : variable_path -> strength
 val find_section_variable : identifier -> variable_path
+val last_section_hyps : dir_path -> identifier list
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant, 
@@ -81,6 +82,9 @@ val find_section_variable : identifier -> variable_path
     [construct_reference] is a version which looks for variables in a 
     given environment instead of looking in the current global environment. *)
 
+val context_of_global_reference : global_reference -> section_context
+val instantiate_inductive_section_params : constr -> inductive_path -> constr
+val implicit_section_args : global_reference -> section_path list
 val extract_instance : global_reference -> constr array -> constr array
 
 val constr_of_reference :
@@ -88,6 +92,7 @@ val constr_of_reference :
 
 val global_qualified_reference : qualid -> constr
 val global_absolute_reference : section_path -> constr
+val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 val construct_qualified_reference : Environ.env -> qualid -> constr
 val construct_absolute_reference : Environ.env -> section_path -> constr
diff --git a/library/global.ml b/library/global.ml
index e5f0d07fd..c07452988 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -35,11 +35,11 @@ let named_context () = named_context !global_env
 let push_named_def idc = global_env := push_named_def idc !global_env
 let push_named_assum idc = global_env := push_named_assum idc !global_env
 
-let add_parameter sp c = global_env := add_parameter sp c !global_env
-let add_constant sp ce = global_env := add_constant sp ce !global_env
-let add_discharged_constant sp r = 
-  global_env := add_discharged_constant sp r !global_env
-let add_mind sp mie = global_env := add_mind sp mie !global_env
+let add_parameter sp c l = global_env := add_parameter sp c l !global_env
+let add_constant sp ce l = global_env := add_constant sp ce l !global_env
+let add_discharged_constant sp r l = 
+  global_env := add_discharged_constant sp r l !global_env
+let add_mind sp mie l = global_env := add_mind sp mie l !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
 let pop_named_decls ids = global_env := pop_named_decls ids !global_env
@@ -87,8 +87,6 @@ let mind_is_recursive =
 
 let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif
 let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif
-let mind_nf_arity x =
-  body_of_type (Inductive.mis_user_arity (lookup_mind_specif x))
 let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif
 
 
diff --git a/library/global.mli b/library/global.mli
index 0ad3e3713..74a7197d4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -26,10 +26,11 @@ val named_context : unit -> named_context
 val push_named_assum : identifier * constr -> unit
 val push_named_def : identifier * constr -> unit
 
-val add_parameter : section_path -> constr -> unit
-val add_constant : section_path -> constant_entry -> unit
-val add_discharged_constant : section_path -> Cooking.recipe -> unit
-val add_mind : section_path -> mutual_inductive_entry -> unit
+val add_parameter : section_path -> constr -> local_names -> unit
+val add_constant : section_path -> constant_entry -> local_names -> unit
+val add_discharged_constant : section_path -> Cooking.recipe -> 
+  local_names -> unit
+val add_mind : section_path -> mutual_inductive_entry -> local_names -> unit
 val add_constraints : constraints -> unit
 
 val pop_named_decls : identifier list -> unit
@@ -61,6 +62,5 @@ val env_of_context : named_context -> env
 val mind_is_recursive : inductive -> bool
 val mind_nconstr : inductive -> int
 val mind_nparams : inductive -> int
-val mind_nf_arity : inductive -> constr
 val mind_nf_lc : inductive -> constr array
 
diff --git a/library/nametab.ml b/library/nametab.ml
index b62f4d867..c8e10a1ed 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -148,15 +148,34 @@ let constant_sp_of_id id =
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let check_absoluteness sp =
-  match dirpath sp with
+let check_absoluteness dir =
+  match dir with
     | a::_ when List.mem a !roots -> ()
-    | _ -> anomaly ("Not an absolute path: "^(string_of_path sp))
+    | _ -> anomaly ("Not an absolute dirpath: "^(string_of_dirpath dir))
 
 let absolute_reference sp =
-  check_absoluteness sp;
+  check_absoluteness (dirpath sp);
   locate (qualid_of_sp sp)
 
+exception Found of global_reference
+let locate_in_module dir id =
+  let rec exists_in id (Closed (ccitab,_,modtab)) =
+    try raise (Found (Stringmap.find id ccitab))
+    with Not_found -> 
+      Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab
+  in
+  let rec search (Closed (ccitab,_,modtab) as mc) = function
+    | modid :: dir' -> search (snd (Stringmap.find modid modtab)) dir'
+    | [] -> 
+	try exists_in id mc; raise Not_found
+	with Found ref -> ref
+  in
+  search !persistent_nametab dir
+
+let locate_in_absolute_module dir id =
+  check_absoluteness dir;
+  locate_in_module dir (string_of_id id)
+
 (* These are entry points to make the contents of a module/section visible *)
 (* in the current env (does not affect the absolute name space `coq_root') *)
 let open_module_contents qid =
@@ -165,7 +184,13 @@ let open_module_contents qid =
 (*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter push_mod_current modtab
 
-let open_section_contents = open_module_contents
+let conditional_push ref = push_cci_current ref (* TODO *)
+
+let open_section_contents qid =
+  let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
+  Stringmap.iter push_cci_current ccitab;
+(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+  Stringmap.iter push_mod_current modtab
 
 let rec rec_open_module_contents qid =
   let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
diff --git a/library/nametab.mli b/library/nametab.mli
index 64cba70c2..08aea7ccc 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -59,3 +59,7 @@ val push_library_root : string -> unit
    especially, constructor/inductive names are turned into internal
    references inside a block of mutual inductive *)
 val absolute_reference : section_path -> global_reference
+
+(* [locate_in_absolute_module dir id] finds [id] in module [dir] or in
+   one of its section/subsection *)
+val locate_in_absolute_module : dir_path -> identifier -> global_reference
diff --git a/toplevel/class.ml b/toplevel/class.ml
index e0ae40af6..4d8e5ba2c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -8,6 +8,7 @@ open Term
 open Inductive
 open Declarations
 open Environ
+open Inductive
 open Lib
 open Classops
 open Declare
@@ -260,18 +261,16 @@ let build_id_coercion idf_opt source =
     | Some c -> c
     | None -> error_not_transparent source in
   let lams,t = Sign.decompose_lam_assum c in
-  let llams = List.length lams in
-  let lams = List.rev lams in
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name (id_of_string "x"),
-		 applistc vs (rel_list 0 llams),
+		 applistc vs (extended_rel_list 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     it_mkProd_wo_LetIn
-      (mkProd (Anonymous, applistc vs (rel_list 0 llams), lift 1 t))
+      (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
@@ -387,7 +386,7 @@ let count_extra_abstractions hyps ids_to_discard =
     List.fold_left
       (fun (hyps,n as sofar) id -> 
 	 match hyps with
-	   | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
+	   | (hyp,None,_)::rest when id = basename hyp ->(rest, n+1)
 	   | _ -> sofar)
       (hyps,0) ids_to_discard
   in n
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 49dd7b887..5a029a0e6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -440,8 +440,11 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
     | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
+	(*
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
+	*)
+        let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NeverDischarge | DischargeAt _ ->
         let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
     | NotDeclare -> apply_tac_not_declare id pft tpo
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index a3c9586a4..42f05a01d 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -23,13 +23,15 @@ open Recordops
 let recalc_sp dir sp =
   let (_,spid,k) = repr_path sp in Names.make_path dir spid k
 
+let rec find_var id = function
+  | [] -> raise Not_found
+  | (sp,b,_)::l -> if basename sp = id then b=None else find_var id l
+
 let build_abstract_list hyps ids_to_discard =
   map_succeed 
     (fun id ->
        try
-	 match lookup_id_value id hyps with
-	   | None -> ABSTRACT
-	   | Some c -> failwith "caugth"
+	 if find_var id hyps then ABSTRACT else failwith "caugth"
        with Not_found -> failwith "caugth")
     ids_to_discard
 
@@ -110,7 +112,8 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
 	  Array.to_list lc))
       mib.mind_packets
   in
-  let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in
+  let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) mib.mind_hyps in
+  let hyps' = map_named_context (expmod_constr oldenv modlist) hyps in
   let (inds',modl) = abstract_inductive ids_to_discard hyps' inds in
   let lmodif_one_mind i = 
     let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in 
@@ -355,15 +358,21 @@ let close_section _ s =
   let newdir = dirpath sec_sp in
   let olddir = wd_of_sp sec_sp in
   let (ops,ids,_) = 
-    List.fold_left 
-      (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
-  in 
+    if Options.immediate_discharge then ([],[],([],[],[]))
+    else
+      List.fold_left 
+	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+  in
+  let ids = last_section_hyps olddir in
   Global.pop_named_decls ids;
   Summary.unfreeze_lost_summaries fs;
   let mc = segment_contents decls in
-  add_anonymous_leaf (in_end_section (sec_sp,mc)); 
-  List.iter process_operation (List.rev ops) 
+  add_anonymous_leaf (in_end_section (sec_sp,mc));
+  if Options.immediate_discharge then ()
+  else
+    List.iter process_operation (List.rev ops)
 
 let save_module_to s f =
   Library.save_module_to segment_contents s f
 
+
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 91d65a5f9..f24051fd1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -77,8 +77,13 @@ let warning_or_error coe err =
   pPNL (hOV 0 [< 'sTR"Warning: "; st >])
 
 (* We build projections *)
-let declare_projections structref coers paramdecls fields =
-  let r = constr_of_reference Evd.empty (Global.env()) structref in
+let declare_projections indsp coers fields =
+  let mispec = Global.lookup_mind_specif (indsp,[||]) in
+  let paramdecls = Inductive.mis_params_ctxt mispec in
+  let paramdecls = 
+    List.map (fun (na,b,t) -> match na with Name id -> (id,b,t) | _ -> assert false)
+      paramdecls in
+  let r = constr_of_reference Evd.empty (Global.env()) (IndRef indsp) in
   let paramargs = List.rev (List.map (fun (id,_,_) -> mkVar id) paramdecls) in
   let rp = applist (r, paramargs) in
   let x = Environ.named_hd (Global.env()) r Anonymous in
@@ -107,6 +112,7 @@ let declare_projections structref coers paramdecls fields =
 	     it_mkNamedLambda_or_LetIn (mkLambda (x, rp, body)) paramdecls in
 	   let name = 
 	     try
+	       let proj = instantiate_inductive_section_params proj indsp in
 	       let cie = { const_entry_body = proj; const_entry_type = None} in
 	       let sp =
 		 declare_constant fi (ConstantEntry cie,NeverDischarge,false)
@@ -122,7 +128,7 @@ let declare_projections structref coers paramdecls fields =
 		 let constr_fi =
 		   constr_of_reference Evd.empty (Global.env()) refi in
 		 if coe then begin
-		   let cl = Class.class_of_ref structref in
+		   let cl = Class.class_of_ref (IndRef indsp) in
 		   Class.try_add_new_coercion_with_source 
 		     refi NeverDischarge cl
 		 end;
@@ -163,13 +169,13 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
       mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];
-     mind_entry_lc = [type_constructor] } in
+      mind_entry_lc = [type_constructor] } in
   let mie =
     { mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations mie in
   let rsp = (sp,0) in (* This is ind path of idstruc *)
-  let sp_projs = declare_projections (IndRef rsp) coers params fields in
+  let sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
   if is_coe then Class.try_add_new_coercion build NeverDischarge;
   Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index ac2c6836e..b678cc3e5 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -12,8 +12,7 @@ open Sign
    [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  global_reference -> bool list -> 
-    named_context -> named_context -> constant_path option list
+  inductive_path -> bool list -> named_context -> constant_path option list
 
 val definition_structure :
    bool * identifier * (identifier * Coqast.t) list *