Transfers to checker ("let"s in inductive arities + Coq root read-only).

- Support for let's in the signature of the arity of an inductive type was
  in the kernel part of commit 12273,
- Support for binding Coq root read-only in -R option was in commit 12220.

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

1 files changed, 10 insertions, 6 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 05ab5a846..f1c8bea2a 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -253,16 +253,20 @@ let get_instantiated_arity (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (Rel(n+p)::l) (p+1)
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
   in 
-  reln [] 1
+  reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let nrealargs = mip.mind_nrealargs in
+  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   applist 
-    (Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+    (Ind ind,
+       List.map (lift mip.mind_nrealargs_ctxt) params
+       @ extended_rel_list 0 realargs)
 
 (* This exception is local *)
 exception LocalArity of (sorts_family * sorts_family * arity_error) option