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

21 files changed, 316 insertions, 128 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