On laisse les LetIn dans les types des constructeurs et des éliminations

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

3 files changed, 36 insertions, 11 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ee5860311..c29d4385d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -272,9 +272,10 @@ let listrec_mconstr env ntypes nparams i indlc =
         | IsLetIn (na,b,t,d) -> 
 	    assert (largs = []);
             if not (noccur_between n ntypes b & noccur_between n ntypes t) then
-	      raise (IllFormedInd (LocalNonPos n));
-            let recarg = check_pos n b in 
-	    check_constr_rec lrec (n+1) d 
+	      check_constr_rec lrec n (subst1 b d)
+	    else
+              let recarg = check_pos n b in 
+	      check_constr_rec lrec (n+1) d 
 
 	| hd ->
 	    if check_head then
@@ -320,8 +321,9 @@ let cci_inductive env env_ar kind nparams finite inds cst =
 	Some (body_of_type ar) in
     let kelim = allowed_sorts issmall isunit ar_sort in
     let lc_bodies = Array.map body_of_type lc in
-    let splayed_lc = Array.map (splay_prod env Evd.empty) lc_bodies in
-    let nf_lc = Array.map (fun (d,b) -> prod_it b d) splayed_lc in
+    let splayed_lc = Array.map (splay_prod_assum env Evd.empty) lc_bodies in
+    let nf_lc = Array.map
+		  (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let nf_typed_lc,user_lc =
       if nf_lc = lc_bodies then lc,None
       else
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c353e4765..0e47053c6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -169,12 +169,15 @@ let betaiotaevar = [BETA;IOTA;EVAR]
 (* Compact Implementation *)
 type flags = int
 let fbeta = 1 and fdelta = 2 and fevar = 4 and feta = 8 and fiota = 16
+							and fletin = 32
 
 let red_beta f = f land fbeta <> 0
 let red_delta f = f land fdelta <> 0
 let red_evar f = f land fevar <> 0
 let red_eta f = f land feta <> 0
 let red_iota f = f land fiota <> 0
+let red_letin f = f land fletin <> 0
+
 
 (* Local *)
 let beta = fbeta
@@ -183,10 +186,11 @@ let betaiota = fbeta lor fiota
 
 (* Contextual *)
 let delta = fdelta lor fevar
-let betadelta = fbeta lor fdelta lor fevar
-let betadeltaeta = fbeta lor fdelta lor fevar lor feta
-let betadeltaiota = fbeta lor fdelta lor fevar lor fiota
-let betadeltaiotaeta = fbeta lor fdelta lor fevar lor fiota lor feta
+let betadelta = fbeta lor fdelta lor fletin lor fevar
+let betadeltaeta = fbeta lor fdelta lor fletin lor fevar lor feta
+let betadeltaiota = fbeta lor fdelta lor fletin lor fevar lor fiota
+let betadeltaiota_nolet = fbeta lor fdelta lor fevar lor fiota
+let betadeltaiotaeta = fbeta lor fdelta lor fletin lor fevar lor fiota lor feta
 let betaiotaevar = fbeta lor fiota lor fevar
 
 (* Beta Reduction tools *)
@@ -271,7 +275,7 @@ let whd_state_gen flags env sigma =
 	  (match constant_opt_value env const with
 	     | Some  body -> whrec (body, stack)
 	     | None -> s)
-      | IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack
+      | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
       | IsAppL (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
@@ -660,12 +664,18 @@ let whd_betadeltaiotaeta_state env sigma =
   whrec
 *)
 
-let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiota e
+let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
 let whd_betadeltaiotaeta_stack env sigma x =
   appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
 let whd_betadeltaiotaeta env sigma x = 
   app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
 
+let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
+let whd_betadeltaiota_nolet_stack env sigma x =
+  appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+let whd_betadeltaiota_nolet env sigma x = 
+  app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
@@ -949,6 +959,17 @@ let splay_prod env sigma =
   in 
   decrec []
 
+let splay_prod_assum env sigma = 
+  let rec prodec_rec l c =
+    let t = whd_betadeltaiota_nolet env sigma c in
+    match kind_of_term c with
+    | IsProd (x,t,c)  -> prodec_rec (Sign.add_rel_decl (x,outcast_type t) l) c
+    | IsLetIn (x,b,t,c) -> prodec_rec (Sign.add_rel_def (x,b,outcast_type t) l) c
+    | IsCast (c,_)    -> prodec_rec l c
+    | _               -> l,c
+  in 
+  prodec_rec Sign.empty_rel_context
+
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
   match kind_of_term c with
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index d1a092ae7..7bb43b055 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -115,6 +115,8 @@ val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
 val decomp_n_prod : 
   env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
+val splay_prod_assum :
+  env -> 'a evar_map -> constr -> Sign.rel_context * constr
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)