Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 179 insertions, 134 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e3457006d0..edb758f078 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Inductive
@@ -21,6 +20,17 @@ open Reduction
 open Typeops
 open Entries
 open Pp
+open Context.Rel.Declaration
+
+(* Terminology:
+paramdecls (ou paramsctxt?)
+args = params + realargs (called vargs when an array, largs when a list)
+params = recparams + nonrecparams
+nonrecargs = nonrecparams + realargs
+env_ar = initial env + declaration of inductive types
+env_ar_par = env_ar + declaration of parameters
+nmr = ongoing computation of recursive parameters
+*)
 
 (* Tell if indices (aka real arguments) contribute to size of inductive type *)
 (* If yes, this is compatible with the univalent model *)
@@ -117,18 +127,18 @@ let is_unit constrsinfos =
    | [] -> (* type without constructors *) true
    | _ -> false
 
-let infos_and_sort env ctx t =
-  let rec aux env ctx t max =
+let infos_and_sort env t =
+  let rec aux env t max =
     let t = whd_betadeltaiota env t in
       match kind_of_term t with
       | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
-	let env1 = Environ.push_rel (name,None,varj.utj_val) env in
+	let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in
 	let max = Universe.sup max (univ_of_sort varj.utj_type) in
-	  aux env1 ctx c2 max
+	  aux env1 c2 max
     | _ when is_constructor_head t -> max
     | _ -> (* don't fail if not positive, it is tested later *) max
-  in aux env ctx t Universe.type0m
+  in aux env t Universe.type0m
 
 (* Computing the levels of polymorphic inductive types
 
@@ -153,14 +163,14 @@ let infos_and_sort env ctx t =
 (* This (re)computes informations relevant to extraction and the sort of an
    arity or type constructor; we do not to recompute universes constraints *)
 
-let infer_constructor_packet env_ar_par ctx params lc =
+let infer_constructor_packet env_ar_par params lc =
   (* type-check the constructors *)
   let jlc = List.map (infer_type env_ar_par) lc in
   let jlc = Array.of_list jlc in
   (* generalize the constructor over the parameters *)
   let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
   (* compute the max of the sorts of the products of the constructors types *)
-  let levels = List.map (infos_and_sort env_ar_par ctx) lc in
+  let levels = List.map (infos_and_sort env_ar_par) lc in
   let isunit = is_unit levels in
   let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
   let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
@@ -169,12 +179,14 @@ let infer_constructor_packet env_ar_par ctx params lc =
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
   fst (List.fold_right
-    (fun (_,b,t as d) (lev,env) ->
-      if Option.is_empty b then
+    (fun d (lev,env) ->
+     match d with
+     | LocalAssum (_,t) ->
 	let tj = infer_type env t in
 	let u = univ_of_sort tj.utj_type in
 	  (Universe.sup u lev, push_rel d env)
-      else lev, push_rel d env)
+     | LocalDef _ ->
+	lev, push_rel d env)
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
@@ -184,15 +196,16 @@ let is_impredicative env u =
    polymorphism. The elements x_k is None if the k-th parameter (starting
    from the most recent and ignoring let-definitions) is not contributing 
    or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls params =
-  let fold acc = function (_, None, p) -> 
+let param_ccls paramsctxt =
+  let fold acc = function
+    | (LocalAssum (_, p)) ->
       (let c = strip_prod_assum p in
       match kind_of_term c with
         | Sort (Type u) -> Univ.Universe.level u
         | _ -> None) :: acc
-    | _ -> acc 
+    | LocalDef _ -> acc
   in
-  List.fold_left fold [] params
+  List.fold_left fold [] paramsctxt
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
@@ -208,7 +221,7 @@ let typecheck_inductive env mie =
   mind_check_names mie;
   (* Params are typed-checked here *)
   let env' = push_context mie.mind_entry_universes env in
-  let (env_params, params) = infer_local_decls env' mie.mind_entry_params in
+  let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
   (* the set of constraints *)
@@ -247,27 +260,26 @@ let typecheck_inductive env mie =
 	    later, after the validation of the inductive definition,
 	    full_arity is used as argument or subject to cast, an
 	    upper universe will be generated *)
-	 let full_arity = it_mkProd_or_LetIn arity params in
+	 let full_arity = it_mkProd_or_LetIn arity paramsctxt in
 	 let id = ind.mind_entry_typename in
 	 let env_ar' =
-           push_rel (Name id, None, full_arity) env_ar in
+           push_rel (LocalAssum (Name id, full_arity)) env_ar in
              (* (add_constraints cst2 env_ar) in *)
-	   (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l))
+	   (env_ar', (id,full_arity,sign @ paramsctxt,expltype,deflev,inflev)::l))
       (env',[])
       mie.mind_entry_inds in
 
   let arity_list = List.rev rev_arity_list in
 
   (* builds the typing context "Gamma, I1:A1, ... In:An, params" *)
-  let env_ar_par = push_rel_context params env_arities in
+  let env_ar_par = push_rel_context paramsctxt env_arities in
 
   (* Now, we type the constructors (without params) *)
   let inds =
     List.fold_right2
       (fun ind arity_data inds ->
 	 let (lc',cstrs_univ) =
-	   infer_constructor_packet env_ar_par ContextSet.empty
-	     params ind.mind_entry_lc in
+	   infer_constructor_packet env_ar_par paramsctxt ind.mind_entry_lc in
 	 let consnames = ind.mind_entry_consnames in
 	 let ind' = (arity_data,consnames,lc',cstrs_univ) in
 	   ind'::inds)
@@ -290,8 +302,7 @@ let typecheck_inductive env mie =
       let full_polymorphic () = 
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
-	  type_in_type env || (check_leq (universes env') infu defu &&
-	    not (is_type0m_univ defu && not is_unit))
+	  type_in_type env || (UGraph.check_leq (universes env') infu defu)
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
@@ -317,14 +328,14 @@ let typecheck_inductive env mie =
 	    (* conclusions of the parameters *)
             (* We enforce [u >= lev] in case [lev] has a strict upper *)
             (* constraints over [u] *)
-	    let b = type_in_type env || check_leq (universes env') infu u in
+	    let b = type_in_type env || UGraph.check_leq (universes env') infu u in
 	      if not b then
 		anomaly ~label:"check_inductive" 
 		  (Pp.str"Incorrect universe " ++
 		     Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
 		   ++ Universe.pr clev)
 	      else
-		TemplateArity (param_ccls params, infu)
+		TemplateArity (param_ccls paramsctxt, infu)
 	  | _ (* Not an explicit occurrence of Type *) ->
 	    full_polymorphic ()
       in
@@ -334,7 +345,7 @@ let typecheck_inductive env mie =
       in
 	(id,cn,lc,(sign,arity)))
     inds
-  in (env_arities, env_ar_par, params, inds)
+  in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
 (************************************************************************)
@@ -343,7 +354,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor
+  | LocalNotConstructor of Context.Rel.t * int
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -354,20 +365,22 @@ exception IllFormedInd of ill_formed_ind
 
 let mind_extract_params = decompose_prod_n_assum
 
-let explain_ind_err id ntyp env nbpar c nargs err =
-  let (lpar,c') = mind_extract_params nbpar c in
+let explain_ind_err id ntyp env nparamsctxt c err =
+  let (lparams,c') = mind_extract_params nparamsctxt c in
   match err with
     | LocalNonPos kt ->
-	raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
+	raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt))))
     | LocalNotEnoughArgs kt ->
 	raise (InductiveError
-		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
-    | LocalNotConstructor ->
+		 (NotEnoughArgs (env,c',mkRel (kt+nparamsctxt))))
+    | LocalNotConstructor (paramsctxt,nargs)->
+        let nparams = Context.Rel.nhyps paramsctxt in
 	raise (InductiveError
-		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
+		 (NotConstructor (env,id,c',mkRel (ntyp+nparamsctxt),
+                                  nparams,nargs)))
     | LocalNonPar (n,i,l) ->
 	raise (InductiveError
-		 (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
+		 (NonPar (env,c',n,mkRel i,mkRel (l+nparamsctxt))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -383,43 +396,50 @@ let failwith_non_pos_list n ntypes l =
   anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
 
 (* Check the inductive type is called with the expected parameters *)
-let check_correct_par (env,n,ntypes,_) hyps l largs =
-  let nparams = rel_context_nhyps hyps in
-  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
-  let nhyps = List.length hyps in
-  let rec check k index = function
+(* [n] is the index of the last inductive type in [env] *)
+let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
+  let nparams = Context.Rel.nhyps paramdecls in
+  let args = Array.of_list args in
+  if Array.length args < nparams then
+    raise (IllFormedInd (LocalNotEnoughArgs ind_index));
+  let (params,realargs) = Array.chop nparams args in
+  let nparamdecls = List.length paramdecls in
+  let rec check param_index paramdecl_index = function
     | [] -> ()
-    | (_,Some _,_)::hyps -> check k (index+1) hyps
-    | _::hyps ->
-        match kind_of_term (whd_betadeltaiota env lpar.(k)) with
-	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1, index, 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'
-
-(* Computes the maximum number of recursive parameters :
-    the first parameters which are constant in recursive arguments
-    n is the current depth, nmr is the maximum number of possible
-    recursive parameters *)
-
-let compute_rec_par (env,n,_,_) hyps nmr largs =
+    | LocalDef _ :: paramdecls ->
+      check param_index (paramdecl_index+1) paramdecls
+    | _::paramdecls ->
+        match kind_of_term (whd_betadeltaiota env params.(param_index)) with
+	  | Rel w when Int.equal w paramdecl_index ->
+            check (param_index-1) (paramdecl_index+1) paramdecls
+	  | _ ->
+            let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in
+            let err =
+              LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in
+            raise (IllFormedInd err)
+  in check (nparams-1) (n-nparamdecls) paramdecls;
+  if not (Array.for_all (noccur_between n ntypes) realargs) then
+    failwith_non_pos_vect n ntypes realargs
+
+(* Computes the maximum number of recursive parameters:
+   the first parameters which are constant in recursive arguments
+   [n] is the current depth, [nmr] is the maximum number of possible
+   recursive parameters *)
+
+let compute_rec_par (env,n,_,_) paramsctxt nmr largs =
 if Int.equal nmr 0 then 0 else
-(* start from 0, hyps will be in reverse order *)
+(* start from 0, params will be in reverse order *)
   let (lpar,_) = List.chop nmr largs in
   let rec find k index =
       function
 	  ([],_) -> nmr
-	| (_,[]) -> assert false (* |hyps|>=nmr *)
-	| (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
-	| (p::lp,_::hyps) ->
+	| (_,[]) -> assert false (* |paramsctxt|>=nmr *)
+	| (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt)
+	| (p::lp,_::paramsctxt) ->
        ( match kind_of_term (whd_betadeltaiota env p) with
-	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps)
+	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt)
           | _ -> k)
-  in find 0 (n-1) (lpar,List.rev hyps)
+  in find 0 (n-1) (lpar,List.rev paramsctxt)
 
 (* [env] is the typing environment
    [n] is the dB of the last inductive type
@@ -428,15 +448,15 @@ if Int.equal nmr 0 then 0 else
    [lra] is the list of recursive tree of each variable
  *)
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+  (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
 
-let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
+let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let auxntyp = 1 in
   let specif = (lookup_mind_specif env mi, u) in
   let ty = type_of_inductive env specif in
   let env' =
-    push_rel (Anonymous,None,
-              hnf_prod_applist env ty lpar) env in
+    let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lrecparams) in
+    push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -456,7 +476,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
 let array_min nmr a = if Int.equal nmr 0 then 0 else
   Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a
 
-(** [check_positivity_one ienv hyps (mind,i) nargs lcnames indlc]
+(** [check_positivity_one ienv paramsctxt (mind,i) nnonrecargs lcnames indlc]
     checks the positivity of the [i]-th member of the mutually
     inductive definition [mind]. It returns an [Rtree.t] which
     represents the position of the recursive calls of inductive in [i]
@@ -464,9 +484,9 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
     considered sub-terms) as well as the number of of non-uniform
     arguments (used to generate induction schemes, so a priori less
     relevant to the kernel). *)
-let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
-  let lparams = rel_context_length hyps in
-  let nmr = rel_context_nhyps hyps in
+let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as ind) nnonrecargs lcnames indlc =
+  let nparamsctxt = Context.Rel.length paramsctxt in
+  let nmr = Context.Rel.nhyps paramsctxt in
   (** Positivity of one argument [c] of a constructor (i.e. the
       constructor [cn] has a type of the shape [… -> c … -> P], where,
       more generally, the arrows may be dependent). *)
@@ -489,7 +509,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
             let largs = List.map (whd_betadeltaiota env) largs in
 	    let nmr1 =
 	      (match ra with
-                  Mrec _ -> compute_rec_par ienv hyps nmr largs
+                  Mrec _ -> compute_rec_par ienv paramsctxt nmr largs
 		|  _ -> nmr)
 	    in
               (** The case where one of the inductives of the mutually
@@ -524,27 +544,27 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
   (* accesses to the environment are not factorised, but is it worth? *)
   and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) =
     let (mib,mip) = lookup_mind_specif env mi in
-    let auxnpar = mib.mind_nparams_rec in
-    let nonrecpar = mib.mind_nparams - auxnpar in
-    let (lpar,auxlargs) =
-      try List.chop auxnpar largs
+    let auxnrecpar = mib.mind_nparams_rec in
+    let auxnnonrecpar = mib.mind_nparams - auxnrecpar in
+    let (auxrecparams,auxnonrecargs) =
+      try List.chop auxnrecpar largs
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
 
       (** Inductives of the inductive block being defined are only
           allowed to appear nested in the parameters of another inductive
           type. Not in the proper indices. *)
-      if not (List.for_all (noccur_between n ntypes) auxlargs) then
-	failwith_non_pos_list n ntypes auxlargs;
+      if not (List.for_all (noccur_between n ntypes) auxnonrecargs) then
+	failwith_non_pos_list n ntypes auxnonrecargs;
       (* Nested mutual inductive types are not supported *)
       let auxntyp = mib.mind_ntypes in
 	if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
 	(* The nested inductive type with parameters removed *)
-	let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in
+	let auxlcvect = abstract_mind_lc auxntyp auxnrecpar mip.mind_nf_lc in
 	  (* Extends the environment with a variable corresponding to
 	     the inductive def *)
-	let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in
+	let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),auxrecparams) in
 	  (* Parameters expressed in env' *)
-	let lpar' = List.map (lift auxntyp) lpar in
+	let auxrecparams' = List.map (lift auxntyp) auxrecparams in
 	let irecargs_nmr =
 	  (** Checks that the "nesting" inductive type is covariant in
 	      the relevant parameters. In other words, that the
@@ -553,9 +573,9 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	      positively in the types of the nested constructors. *)
 	  Array.map
 	    (function c ->
-	      let c' = hnf_prod_applist env' c lpar' in
+	      let c' = hnf_prod_applist env' c auxrecparams' in
 	      (* skip non-recursive parameters *)
-	      let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in
+	      let (ienv',c') = ienv_decompose_prod ienv' auxnnonrecpar c' in
 		check_constructors ienv' false nmr c')
 	    auxlcvect
 	in
@@ -579,6 +599,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
+	      if not recursive && not (noccur_between n ntypes b) then
+	        raise (InductiveError BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
                 check_constr_rec ienv' nmr' (recarg::lrec) d
@@ -587,8 +609,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
               if check_head then
                 begin match hd with
                 | Rel j when Int.equal j (n + ntypes - i - 1) ->
-                  check_correct_par ienv hyps (ntypes - i) largs
-                | _ -> raise (IllFormedInd LocalNotConstructor)
+                  check_correct_par ienv paramsctxt (ntypes - i) largs
+                | _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs)))
                 end
               else
                 if not (List.for_all (noccur_between n ntypes) largs)
@@ -600,31 +622,32 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
   let irecargs_nmr =
     Array.map2
       (fun id c ->
-        let _,rawc = mind_extract_params lparams c in
+        let _,rawc = mind_extract_params nparamsctxt c in
           try
 	    check_constructors ienv true nmr rawc
           with IllFormedInd err ->
-	    explain_ind_err id (ntypes-i) env lparams c nargs err)
+	    explain_ind_err id (ntypes-i) env nparamsctxt c err)
       (Array.of_list lcnames) indlc
   in
   let irecargs = Array.map snd irecargs_nmr
   and nmr' = array_min nmr irecargs_nmr
   in (nmr', mk_paths (Mrec ind) irecargs)
 
-(** [check_positivity kn env_ar params] checks that the mutually
+(** [check_positivity kn env_ar paramsctxt inds] checks that the mutually
     inductive block [inds] is strictly positive. *)
-let check_positivity kn env_ar params inds =
+let check_positivity kn env_ar_par paramsctxt finite inds =
   let ntypes = Array.length inds in
+  let recursive = finite != Decl_kinds.BiFinite in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
-  let lra_ind = Array.rev_to_list rc in
-  let lparams = rel_context_length params in
-  let nmr = rel_context_nhyps params in
+  let ra_env_ar = Array.rev_to_list rc in
+  let nparamsctxt = Context.Rel.length paramsctxt in
+  let nmr = Context.Rel.nhyps paramsctxt in
   let check_one i (_,lcnames,lc,(sign,_)) =
-    let ra_env =
-      List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
-    let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-    let nargs = rel_context_nhyps sign - nmr in
-    check_positivity_one ienv params (kn,i) nargs lcnames lc
+    let ra_env_ar_par =
+      List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in
+    let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in
+    let nnonrecargs = Context.Rel.nhyps sign - nmr in
+    check_positivity_one recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
   let irecargs = Array.map snd irecargs_nmr
@@ -681,6 +704,7 @@ let used_section_variables env inds =
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+let rel_list n m = Array.to_list (rel_vect n m)
 
 exception UndefinableExpansion
 
@@ -695,24 +719,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
   let indty, paramsletsubst =
-    let subst, inst = 
-      List.fold_right
-	(fun (na, b, t) (subst, inst) ->
-	 match b with
-	 | None -> (mkRel 1 :: List.map (lift 1) subst,
-		   mkRel 1 :: List.map (lift 1) inst)
-	 | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
-	paramslet ([], [])
-    in
+    (* [ty] = [Ind inst] is typed in context [params] *)
+    let inst = Context.Rel.to_extended_vect 0 paramslet in
+    let ty = mkApp (mkIndU indu, inst) in
+    (* [Ind inst] is typed in context [params-wo-let] *)
+    let inst' = rel_list 0 nparamargs in
+    (* {params-wo-let |- subst:params] *)
+    let subst = subst_of_rel_context_instance paramslet inst' in
+    (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
     let subst = (* For the record parameter: *)
-      mkRel 1 :: List.map (lift 1) subst
-    in
-    let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+      mkRel 1 :: List.map (lift 1) subst in
       ty, subst
   in
   let ci = 
     let print_info =
-      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
 	ci_npar    = nparamargs;
 	ci_cstr_ndecls = mind_consnrealdecls;
@@ -730,16 +751,39 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
       it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
   in
-  let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
-    match b with
-    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
-		substl letsubst c :: subst)
-    | None ->
+  let projections decl (i, j, kns, pbs, subst, letsubst) =
+    match decl with
+    | LocalDef (na,c,t) ->
+        (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+        let c = liftn 1 j c in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c1 = substl subst c in
+        (* From [params, x:I |- subst:field1,..,fieldj]
+           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+           is represented with instance of field1 last *)
+        let subst = c1 :: subst in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c2 = substl letsubst c in
+        (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
+           to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
+        let letsubst = c2 :: letsubst in
+        (i, j+1, kns, pbs, subst, letsubst)
+    | LocalAssum (na,t) ->
       match na with
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
-	let projty = substl letsubst (liftn 1 j t) in
-	let ty = substl subst (liftn 1 j t) in
+        (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+        let t = liftn 1 j t in
+        (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+	let projty = substl letsubst t in
+        (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+           to [params, x:I |- t(proj1 x,..,projj x)] *)
+	let ty = substl subst t in
 	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
@@ -758,14 +802,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
-let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
+let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
-  let nparamargs = rel_context_nhyps params in
-  let nparamdecls = rel_context_length params in
+  let nparamargs = Context.Rel.nhyps paramsctxt in
+  let nparamsctxt = Context.Rel.length paramsctxt in
   let subst, ctx = Univ.abstract_universes p ctx in
-  let params = Vars.subst_univs_level_context subst params in
+  let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in
   let env_ar = 
     let ctx = Environ.rel_context env_ar in 
     let ctx' = Vars.subst_univs_level_context subst ctx in
@@ -778,10 +822,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let consnrealdecls =
-      Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
+      Array.map (fun (d,_) -> Context.Rel.length d - nparamsctxt)
 	splayed_lc in
     let consnrealargs =
-      Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+      Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs)
 	splayed_lc in
     (* Elimination sorts *)
     let arkind,kelim = 
@@ -814,8 +858,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       { mind_typename = id;
 	mind_arity = arkind;
 	mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
-	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-	mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
+	mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
+	mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealdecls;
@@ -828,10 +872,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
-  let pkt = packets.(0) in	  
+  let pkt = packets.(0) in
   let isrecord = 
     match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+    | Some (Some rid) when pkt.mind_kelim == all_sorts
+			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u = 
@@ -844,7 +889,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	(try 
 	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
-	     compute_projections indsp pkt.mind_typename rid nparamargs params
+	     compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
@@ -858,7 +903,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       mind_hyps = hyps;
       mind_nparams = nparamargs;
       mind_nparams_rec = nmr;
-      mind_params_ctxt = params;
+      mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_polymorphic = p;
       mind_universes = ctx;
@@ -870,11 +915,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
+  let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
+  let (nmr,recargs) = check_positivity kn env_ar_par paramsctxt mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
-      env_ar params kn mie.mind_entry_record mie.mind_entry_finite
+      env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs