Ajout d'un LetIn primitif.

Abstraction de constr via kind_of_constr dans une bonne partie du code.


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

7 files changed, 149 insertions, 155 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 853798daba..5415d819cf 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Sign
-open Generic
+(*i open Generic i*)
 open Term
 open Environ
 open Evd
@@ -278,17 +278,6 @@ let dbize k sigma env allow_soapp lvar =
   let rec dbrec env = function
     | Nvar(loc,s) -> fst (dbize_ref k sigma env loc s lvar)
 	  
-   (*
-   | Slam(_,ona,Node(_,"V$",l)) ->
-       let na =
-         (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-       in DLAMV(na,Array.of_list (List.map (dbrec (Idset.add na env)) l))
-
-   | Slam(_,ona,t) ->
-       let na =
-         (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-       in DLAM(na, dbrec (Idset.add na env) t)
-   *)
     | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
 	let (lf,ln,lA,lt) = dbize_fix ldecl in
 	let n =
@@ -313,13 +302,17 @@ let dbize k sigma env allow_soapp lvar =
 	  List.fold_left (fun env fid -> Idset.add fid env) env lf in
 	let defl = Array.of_list (List.map (dbrec ext_env) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
-	RRec (loc,RCofix n, Array.of_list lf, arityl, defl)
+	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
 	  
-    | Node(loc,("PROD"|"LAMBDA" as k), [c1;Slam(_,ona,c2)]) ->
+    | Node(loc,("PROD"|"LAMBDA"|"LETIN" as k), [c1;Slam(_,ona,c2)]) ->
 	let na,env' = match ona with
 	  | Some s -> let id = id_of_string s in Name id, Idset.add id env
 	  | _ -> Anonymous, env in
-	let kind = if k="PROD" then BProd else BLambda in
+	let kind = match k with
+	  | "PROD" -> BProd
+	  | "LAMBDA" -> BLambda
+	  | "LETIN" -> BLetIn
+	  | _ -> assert false in
 	RBinder(loc, kind, na, dbrec env c1, dbrec env' c2)
 
     | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> 
@@ -401,12 +394,12 @@ let dbize k sigma env allow_soapp lvar =
     | Slam(loc,ona,body) ->
 	let na,env' = match ona with 
 	  | Some s ->
-	      check_capture s ty body;
+	      if n>0 then check_capture s ty body;
 	      let id = id_of_string s in Name id, Idset.add id env
 	  | _ -> Anonymous, env
 	in
 	RBinder(loc, oper, na, dbrec env ty,
-		(iterated_binder oper n ty env' body))
+		(iterated_binder oper (n+1) ty env' body))
     | body -> dbrec env body
 
   and dbize_args env l args =
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index b8534a8730..03af08edc8 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -77,16 +77,19 @@ GEXTEND Gram
 	  <:ast< (LocateLibrary $id) >>
       | IDENT "Locate"; id = identarg; "." ->
 	  <:ast< (Locate $id) >>
-      | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
+
+       (* For compatibility (now turned into a table) *)
       | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
       | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
+      | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
       | IDENT "AddRecPath"; dir = stringarg; "." ->
           <:ast< (RECADDPATH $dir) >>
+	  
       | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >>
       | IDENT "Print"; "Proof"; id = identarg; "." ->
           <:ast< (PrintOpaqueId $id) >>
-(* Pris en compte dans PrintOption ci-dessous 
-      | IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >> *)
+(* Pris en compte dans PrintOption ci-dessous (CADUC) *)
+      | IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >>
       | IDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >>
       | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
       (* TODO: rapprocher Eval et Check *)
@@ -110,7 +113,7 @@ GEXTEND Gram
       | IDENT "Print"; IDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
       | IDENT "Print"; IDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
       | IDENT "Print"; IDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
-      | IDENT "Print"; IDENT "Path"; c = identarg; d = identarg; "." ->
+      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg; "." ->
           <:ast< (PrintPATH $c $d) >>
 
       | IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
@@ -138,22 +141,35 @@ GEXTEND Gram
           <:ast< (SetTableField $table) >>
       | IDENT "Unset"; table = identarg; "." ->
           <:ast< (UnsetTableField $table) >>
-      | IDENT "Print"; table = identarg; field = identarg; "." ->
+      | IDENT "Print"; IDENT "Table";
+		      table = identarg; field = identarg; "." ->
           <:ast< (PrintOption $table $field) >>
       (* Le cas suivant inclut aussi le "Print id" standard *)
-      | IDENT "Print"; table = identarg; "." ->
+      | IDENT "Print"; IDENT "Table"; table = identarg; "." ->
           <:ast< (PrintOption $table) >>
       | IDENT "Add"; table = identarg; field = identarg; id = identarg; "."
         -> <:ast< (AddTableField $table $field $id) >>
+      | IDENT "Add"; table = identarg; field = identarg; id = stringarg; "."
+        -> <:ast< (AddTableField $table $field $id) >>
       | IDENT "Add"; table = identarg; id = identarg; "."
         -> <:ast< (AddTableField $table $id) >>
+      | IDENT "Add"; table = identarg; id = stringarg; "."
+        -> <:ast< (AddTableField $table $id) >>
       | IDENT "Test"; table = identarg; field = identarg; id = identarg; "."
         -> <:ast< (MemTableField $table $field $id) >>
+      | IDENT "Test"; table = identarg; field = identarg; id = stringarg; "."
+        -> <:ast< (MemTableField $table $field $id) >>
       | IDENT "Test"; table = identarg; id = identarg; "."
         -> <:ast< (MemTableField $table $id) >>
+      | IDENT "Test"; table = identarg; id = stringarg; "."
+        -> <:ast< (MemTableField $table $id) >>
       | IDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
           <:ast< (RemoveTableField $table $field $id) >>
+      | IDENT "Remove"; table = identarg; field = identarg; id = stringarg; "." ->
+          <:ast< (RemoveTableField $table $field $id) >>
       | IDENT "Remove"; table = identarg; id = identarg; "." ->
+          <:ast< (RemoveTableField $table $id) >>
+      | IDENT "Remove"; table = identarg; id = stringarg; "." ->
           <:ast< (RemoveTableField $table $id) >> ] ]
   ;
   option_value:
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index d685b292a0..2a7f5ac8e6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -84,8 +84,9 @@ GEXTEND Gram
         c = constr; "in"; c1 = constr ->
           <:ast< (CASE "NOREC" "SYNTH" $c (LAMBDALIST (ISEVAR)
                    ($SLAM $b $c1))) >>
-      | IDENT "let"; id1 = IDENT ; "="; c = constr; "in";
-        c1 = constr -> <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>
+      | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> 
+	  <:ast< (LETIN $c [$id1]$c1) >>
+(* <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>*)
       | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
         IDENT "else"; c3 = constr ->
         <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >>
@@ -141,11 +142,13 @@ GEXTEND Gram
     [ [ ","; idl = ne_ident_comma_list -> idl
       | -> [] ] ]
   ;
-  vardecls:
+  vardecls: (* This is interpreted by Pcoq.abstract_binder *)
     [ [ id = ident; idl = ident_comma_list_tail; c = type_option ->
           <:ast< (BINDER $c $id ($LIST $idl)) >>
+      | id = ident; ":="; c = constr ->
+	  <:ast< (LETIN $c $id) >>
       | id = ident; "="; c = constr ->
-	  <:ast< (ABST #Core#let.cci $c $id) >> ] ]
+	  <:ast< (LETIN $c $id) >> ] ]
   ;
   ne_vardecls_list:
     [ [ id = vardecls; ";"; idl = ne_vardecls_list -> id :: idl
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index e3fa611eda..ff747d4e35 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Util
-open Generic
+(*i open Generic i*)
 open Names
 open Term
 open Reduction
@@ -14,7 +14,6 @@ type constr_pattern =
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of int * constr_pattern list
   | PBinder of binder_kind * name * constr_pattern * constr_pattern
-  | PLet of identifier * constr_pattern * constr_pattern * constr_pattern
   | PSort of rawsort
   | PMeta of int option
   | PCase of constr_pattern option * constr_pattern * constr_pattern array
@@ -32,9 +31,6 @@ let rec occur_meta_pattern = function
   | PCase(Some p,c,br) ->
       (occur_meta_pattern p) or
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
-  | PLet(id,a,t,c)  ->
-      (occur_meta_pattern a) or (occur_meta_pattern t)
-      or (occur_meta_pattern c)
   | PMeta _ | PSoApp _ -> true
   | PRel _ | PSort _   -> false
 
@@ -62,10 +58,9 @@ let label_of_ref = function
 
 let rec head_pattern_bound t =
   match t with
-    | PBinder (BProd,_,_,b) -> head_pattern_bound b 
+    | PBinder ((BProd|BLetIn),_,_,b) -> head_pattern_bound b 
     | PApp (c,args)         -> head_pattern_bound c
     | PCase (p,c,br)        -> head_pattern_bound c
-    | PLet (id,a,t,c)       -> head_pattern_bound c
     | PRef r                -> label_of_ref r
     | PRel _ | PMeta _ | PSoApp _  | PSort _ -> raise BoundPattern
     | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type"
@@ -96,7 +91,7 @@ let head_of_constr_reference = function
    When we reach a second-order application, we ask that the
    intersection of the free-rels of the term and the current stack be
    contained in the arguments of the application, and in that case, we
-   construct a DLAM with the names on the stack.
+   construct a LAMBDA with the names on the stack.
 
  *)
 
@@ -109,12 +104,12 @@ let constrain ((n : int),(m : constr)) sigma =
   else 
     (n,m)::sigma
     
-let build_dlam toabstract stk (m : constr) = 
+let build_lambda toabstract stk (m : constr) = 
   let rec buildrec m p_0 p_1 = match p_0,p_1 with 
     | (_, []) -> m
-    | (n, (na::tl)) -> 
+    | (n, (na,t)::tl) -> 
 	if List.mem n toabstract then
-          buildrec (DLAM(na,m)) (n+1) tl
+          buildrec (mkLambda (na,t,m)) (n+1) tl
         else 
 	  buildrec (pop m) (n+1) tl
   in 
@@ -140,7 +135,7 @@ let matches_core convert pat c =
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
-	    constrain (n,build_dlam relargs stk cT) sigma
+	    constrain (n,build_lambda relargs stk cT) sigma
 	  else
 	    raise PatternMatchingFailure
 
@@ -176,10 +171,13 @@ let matches_core convert pat c =
 	    arg1 (Array.of_list arg2)
 
       | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) ->
-	  sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2
+	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
 
       | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) ->
-	  sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2
+	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
+
+      | PBinder(BLetIn,na1,c1,d1), IsLetIn(na2,c2,t2,d2) ->
+	  sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
 
       | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) 
           when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma
@@ -194,7 +192,7 @@ let matches_core convert pat c =
 	  array_fold_left2 (sorec stk) (sorec stk sigma a1 a2)
 	    br1 br2
 
-      | (PLet _,_) | _,(IsFix _ | IsCoFix _) ->
+      | _,(IsFix _ | IsCoFix _) ->
 	  error "somatch: not implemented"
 
       | _ -> raise PatternMatchingFailure
@@ -222,45 +220,57 @@ let rec try_matches nocc pat = function
 
 (* Tries to match a subterm of [c] with [pat] *)
 let rec sub_match nocc pat c =
-  match c with
-  | DOP2 (Cast,c1,c2) ->
+  match kind_of_term c with
+  | IsCast (c1,c2) ->
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1] in
-      (lm,DOP2 (Cast,List.hd lc,c2))
+      (lm,mkCast (List.hd lc, c2))
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
-      (lm,DOP2 (Cast,List.hd lc,c2)))
-  | DOP2 (ne,c1,DLAM (x,c2)) ->
+      (lm,mkCast (List.hd lc, c2)))
+  | IsLambda (x,c1,c2) ->
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,DOP2 (ne,List.hd lc,DLAM (x,List.nth lc 1)))
+      (lm,mkLambda (x,List.hd lc,List.nth lc 1))
     | NextOccurrence nocc ->
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,DOP2 (ne,List.hd lc,DLAM (x,List.nth lc 1))))
-  | DOPN (AppL,a) when Array.length a <> 0 ->
-    let c1 = a.(0)
-    and lc = List.tl (Array.to_list a) in
+      (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
+  | IsProd (x,c1,c2) ->
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::lc) in
-      (lm,DOPN (AppL,Array.of_list le))
+      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
+      (lm,mkProd (x,List.hd lc,List.nth lc 1))
     | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in
-      (lm,DOPN (AppL,Array.of_list le)))
-  | DOPN (MutCase ci,v) ->
-    let hd = v.(0)
-    and c1 = v.(1)
-    and lc = Array.to_list (Array.sub v 2 (Array.length v - 2)) in
+      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
+      (lm,mkProd (x,List.hd lc,List.nth lc 1)))
+  | IsLetIn (x,c1,t2,c2) ->
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure ->
+      let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
+      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
+    | NextOccurrence nocc ->
+      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
+      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
+  | IsAppL (c1,lc) ->
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure ->
       let (lm,le) = try_sub_match nocc pat (c1::lc) in
-      (lm,DOPN (MutCase ci,Array.of_list (hd::le)))
+      (lm,mkAppL (Array.of_list le))
     | NextOccurrence nocc ->
       let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in
-      (lm,DOPN (MutCase ci,Array.of_list (hd::le))))
-  | c ->
+      (lm,mkAppL (Array.of_list le)))
+  | IsMutCase (ci,hd,c1,lc) ->
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure ->
+      let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
+      (lm,mkMutCase (ci,hd,List.hd le,List.tl le))
+    | NextOccurrence nocc ->
+      let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
+      (lm,mkMutCase (ci,hd,List.hd le,List.tl le)))
+  | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
+  | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _|IsAbst (_, _) ->
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure -> raise (NextOccurrence nocc)
     | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
@@ -295,6 +305,8 @@ let rec pattern_of_constr t =
     | IsSort (Prop c) -> PSort (RProp c)
     | IsSort (Type _) -> PSort RType
     | IsCast (c,_)      -> pattern_of_constr c
+    | IsLetIn (na,c,_,b)   ->
+	PBinder (BLetIn,na,pattern_of_constr c,pattern_of_constr b)
     | IsProd (na,c,b)   ->
 	PBinder (BProd,na,pattern_of_constr c,pattern_of_constr b)
     | IsLambda (na,c,b) ->
diff --git a/parsing/pattern.mli b/parsing/pattern.mli
index 803e4fffea..5506e070d4 100644
--- a/parsing/pattern.mli
+++ b/parsing/pattern.mli
@@ -14,7 +14,6 @@ type constr_pattern =
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of int * constr_pattern list
   | PBinder of binder_kind * name * constr_pattern * constr_pattern
-  | PLet of identifier * constr_pattern * constr_pattern * constr_pattern
   | PSort of Rawterm.rawsort
   | PMeta of int option
   | PCase of constr_pattern option * constr_pattern * constr_pattern array
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 28c4cb3a9f..123f690a8b 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Declarations
 open Inductive
@@ -298,10 +298,12 @@ let print_full_context_typ () = print_context false (Lib.contents_after None)
    assume that the declaration of constructors and eliminations
    follows the definition of the inductive type *)
 
-let rec head_const c = match strip_outer_cast c with
-  | DOP2(Prod,_,DLAM(_,c)) -> head_const c
-  | DOPN(AppL,cl)    -> head_const (array_hd cl)
-  | def         -> def
+let rec head_const c = match kind_of_term c with
+  | IsProd (_,_,d) -> head_const d
+  | IsLetIn (_,_,_,d) -> head_const d
+  | IsAppL (f,_)   -> head_const f
+  | IsCast (d,_)   -> head_const d
+  | _            -> c
 
 let list_filter_vec f vec = 
   let rec frec n lf = 
@@ -488,11 +490,11 @@ let fprint_judge {uj_val=trm;uj_type=typ} =
   [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >]
 
 let unfold_head_fconst = 
-  let rec unfrec = function
-    | DOPN(Const _,_) as k -> constant_value (Global.env ()) k 
-    | DOP2(Lambda,t,DLAM(na,b)) -> DOP2(Lambda,t,DLAM(na,unfrec b))
-    | DOPN(AppL,v) -> DOPN(AppL,array_cons (unfrec (array_hd v)) (array_tl v))
-    | x -> x
+  let rec unfrec k = match kind_of_term k with
+    | IsConst _ -> constant_value (Global.env ()) k 
+    | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b)
+    | IsAppL (f,v) -> applist (unfrec f,v)
+    | _ -> k
   in 
   unfrec
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index ff8222e4ea..98aed4f567 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Univ
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Inductive
 open Sign
@@ -217,6 +217,8 @@ let rec ast_of_raw = function
   | RBinder (_,BProd,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
       ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
+  | RBinder (_,BLetIn,na,t,c) ->
+      ope("LETIN",[ast_of_raw t; slam(stringopt_of_name na,ast_of_raw c)])
   | RBinder (_,bk,na,t,c) ->
       let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
       let tag = match bk with
@@ -226,6 +228,7 @@ let rec ast_of_raw = function
 	  (* non dépendant, pour isoler l'implication; peut-être un *)
 	  (* constructeur ARROW serait-il plus justifié ? *) 
 	| BProd -> if n=1 then "PROD" else "PRODLIST" 
+	| BLetIn -> if n=1 then "LETIN" else "LETINLIST" 
       in
       ope(tag,[ast_of_raw t;a])
 
@@ -270,7 +273,7 @@ let rec ast_of_raw = function
 		 alfi
 	     in 
 	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
-	 | RCofix n -> 
+	 | RCoFix n -> 
 	     let listdecl =
                Array.mapi 
 		 (fun i fi ->
@@ -345,9 +348,11 @@ let occur_id env id0 c =
     | DOPN(_,cl)         -> array_exists (occur n) cl
     | DOP1(_,c)          -> occur n c
     | DOP2(_,c1,c2)      -> (occur n c1) or (occur n c2)
-    | DOPL(_,cl)         -> List.exists (occur n) cl
     | DLAM(_,c)          -> occur (n+1) c
     | DLAMV(_,v)         -> array_exists (occur (n+1)) v
+    | CLam (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
+    | CPrd (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
+    | CLet (_,b,t,c) -> occur n b or occur n (body_of_type t) or occur (n+1) c
     | Rel p              ->
     	p>n &
     	(try lookup_name_of_rel (p-n) env = Name id0
@@ -366,33 +371,26 @@ let next_name_not_occuring name l env t =
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let concrete_name islam l env n c =
-  if n = Anonymous & not (dependent (Rel 1) c) then
+  if n = Anonymous & not (dependent (mkRel 1) c) then
     (None,l)
   else
     let fresh_id = next_name_not_occuring n l env c in
     let idopt =
-      if islam or dependent (Rel 1) c then (Some fresh_id) else None in
+      if islam or dependent (mkRel 1) c then (Some fresh_id) else None in
     (idopt, fresh_id::l)
 
     (* Returns the list of global variables and constants in a term *)
 let global_vars_and_consts t =
-  let rec collect acc = function
-    | VAR id             -> id::acc
-    | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
-    | DOPN (Abst sp,cl)  -> (basename sp)::(Array.fold_left collect acc cl)
-    | DOPN (MutInd ind_sp, cl) as t       -> 
-	(basename (path_of_inductive_path ind_sp))
-	::(Array.fold_left collect acc cl)
-    | DOPN (MutConstruct cstr_sp, cl) as t -> 
-	(basename (path_of_constructor_path cstr_sp))
-	::(Array.fold_left collect acc cl)
-    | DOPN(_,cl)         -> Array.fold_left collect acc cl
-    | DOP1(_,c)          -> collect acc c
-    | DOP2(_,c1,c2)      -> collect (collect acc c1) c2
-    | DOPL(_,cl)         -> List.fold_left collect acc cl
-    | DLAM(_,c)          -> collect acc c
-    | DLAMV(_,v)         -> Array.fold_left collect acc v
-    | _                  -> acc
+  let rec collect acc c =
+    let op, cl = splay_constr c in
+    let acc' = Array.fold_left collect acc cl in
+    match op with
+    | OpVar id -> id::acc'
+    | OpConst sp -> (basename sp)::acc'
+    | OpAbst sp  -> (basename sp)::acc'
+    | OpMutInd ind_sp -> (basename (path_of_inductive_path ind_sp))::acc'
+    | OpMutConstruct csp -> (basename (path_of_constructor_path csp))::acc'
+    | _ -> acc'
   in
   list_uniquize (collect [] t)
     
@@ -403,40 +401,6 @@ let used_of = global_vars_and_consts
 (* These functions implement a light form of Termenv.mind_specif_of_mind    *)
 (* specially for handle Cases printing; they respect arities but not typing *)
 
-(*
-let mind_specif_of_mind_light (sp,tyi) =
-  let mib = Global.lookup_mind sp in
-  (mib,mind_nth_type_packet mib tyi)
-
-let rec remove_indtypes = function
-  | (1, DLAMV(_,cl)) -> cl
-  | (n, DLAM (_,c))  -> remove_indtypes (n-1, c)
-  | _                -> anomaly "remove_indtypes: bad list of constructors"
-
-let rec remove_params n t =
-  if n = 0 then 
-    t
-  else 
-    match t with
-      | DOP2(Prod,_,DLAM(_,c)) -> remove_params (n-1) c
-      | DOP2(Cast,c,_)         -> remove_params n c
-      | _ -> anomaly "remove_params : insufficiently quantified"
-
-let rec get_params = function
-  | DOP2(Prod,_,DLAM(x,c)) -> x::(get_params c)
-  | DOP2(Cast,c,_)         -> get_params c
-  | _                      -> []
-
-let lc_of_lmis (mib,mip) =
-  let lc = remove_indtypes (mib.mind_ntypes,mip.mind_lc) in
-  Array.map (remove_params mib.mind_nparams) lc
-
-let sp_of_spi ((sp,_) as spi) =
-  let (_,mip) = mind_specif_of_mind_light spi in
-  let (pa,_,k) = repr_path sp in 
-  make_path pa (mip.mind_typename) k
-*)	    
-
 let bdize_app c al =
   let impl =
     match c with
@@ -471,13 +435,13 @@ let computable p k =
        sinon on perd la réciprocité de la synthèse (qui, lui,
        engendrera un prédicat non dépendant) *)
 
-  let rec striprec = function
-    | (0,DOP2(Lambda,_,DLAM(_,d))) -> false
-    | (0,d               )         -> noccur_between 1 k d
-    | (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
-    |  _                           -> false
+  let rec striprec n c = match n,kind_of_term c with
+    | (0,IsLambda (_,_,d)) -> false
+    | (0,_)                -> noccur_between 1 k c
+    | (n,IsLambda (_,_,d)) -> striprec (n-1) d
+    |  _                   -> false
   in 
-  striprec (k,p)
+  striprec k p
 
 let ids_of_var cl =
   List.map
@@ -500,7 +464,7 @@ let old_bdize at_top env t =
            | (None,avoid') -> 
 	       slam(None,bdrec avoid' env (pop c)))
     | DLAMV(na,cl) ->
-	if not(array_exists (dependent (Rel 1)) cl) then
+	if not(array_exists (dependent (mkRel 1)) cl) then
 	  slam(None,ope("V$",array_map_to_list
 			  (fun c -> bdrec avoid env (pop c)) cl))
 	else
@@ -535,6 +499,9 @@ let old_bdize at_top env t =
 		 bdrec avoid env c1 
 	       else 
 		 ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
+	   | IsLetIn (na,b,_,c) ->
+	       ope("LETIN",[bdrec [] env b;
+			   slam(stringopt_of_name na,bdrec avoid env (pop c))])
 	   | IsProd (Anonymous,ty,c) ->
                     (* Anonymous product are never factorized *)
 	       ope("PROD",[bdrec [] env ty;
@@ -612,36 +579,38 @@ let old_bdize at_top env t =
 		   (fun env id -> add_name (Name id) env) env lfi in
 	       let def_avoid = lfi@avoid in
 	       let f = List.nth lfi n in
-	       let rec split_lambda binds env avoid = function
-		 | (0, t) -> (binds,bdrec avoid env t)
-		 | (n, DOP2(Cast,t,_)) -> split_lambda binds env avoid (n,t)
-		 | (n, DOP2(Lambda,t,DLAM(na,b))) ->
+	       let rec split_lambda binds env avoid n t =
+		 match (n,kind_of_term t) with
+		 | (0, _) -> (binds,bdrec avoid env t)
+		 | (n, IsCast (t,_)) -> split_lambda binds env avoid n t
+		 | (n, IsLambda (na,t,b)) ->
 		     let ast = bdrec avoid env t in
 		     let id = next_name_away na avoid in
 		     let ast_of_bind = 
 		       ope("BINDER",[ast;nvar (string_of_id id)]) in
 		     let new_env = add_name (Name id) env in
 		     split_lambda (ast_of_bind::binds) 
-		       new_env (id::avoid) (n-1,b)
+		       new_env (id::avoid) (n-1) b
 		 | _ -> error "split_lambda" 
 	       in
-	       let rec split_product env avoid = function
-		 | (0, t) -> bdrec avoid env t
-		 | (n, DOP2(Cast,t,_)) -> split_product env avoid (n,t)
-		 | (n, DOP2(Prod,t,DLAM(na,b))) ->
+	       let rec split_product env avoid n t =
+		 match (n,kind_of_term t) with
+		 | (0, _) -> bdrec avoid env t
+		 | (n, IsCast (t,_)) -> split_product env avoid n t
+		 | (n, IsProd (na,t,b)) ->
 		     let ast = bdrec avoid env t in
 		     let id = next_name_away na avoid in
 		     let new_env = add_name (Name id) env in
-		     split_product new_env (id::avoid) (n-1,b)
+		     split_product new_env (id::avoid) (n-1) b
 		 | _ -> error "split_product" 
 	       in
 	       let listdecl = 
 		 list_map_i
 		   (fun i fi ->
 		      let (lparams,ast_of_def) =
-			split_lambda [] def_env def_avoid (nv.(i)+1,vt.(i)) in
+			split_lambda [] def_env def_avoid (nv.(i)+1) vt.(i) in
 		      let ast_of_typ = 
-			split_product env avoid (nv.(i)+1,cl.(i)) in
+			split_product env avoid (nv.(i)+1) cl.(i) in
 		      ope("FDECL",
 			  [nvar (string_of_id fi); 
 			   ope ("BINDERS",List.rev lparams);
@@ -680,7 +649,7 @@ let old_bdize at_top env t =
 
       | n, DOP2(Lambda,_,DLAM(x,b))
 	-> let x'=
-          if not print_underscore or (dependent (Rel 1) b) then x 
+          if not print_underscore or (dependent (mkRel 1) b) then x 
           else Anonymous in
            let id = next_name_away x' avoid in
            let new_env = (add_name (Name id) env) in
@@ -769,6 +738,10 @@ let rec ast_of_pattern env = function
       ope("SOAPP",(ope ("META",[num n])):: 
 		  (List.map (ast_of_pattern env) args))
 
+  | PBinder (BLetIn,na,b,c) ->
+      let c' = ast_of_pattern (add_name na env) c in
+      ope("LETIN",[ast_of_pattern env b;slam(stringopt_of_name na,c')])
+		
   | PBinder (BProd,Anonymous,t,c) ->
       ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
   | PBinder (bk,na,t,c) ->
@@ -782,14 +755,10 @@ let rec ast_of_pattern env = function
 	  (* non dépendant, pour isoler l'implication; peut-être un *)
 	  (* constructeur ARROW serait-il plus justifié ? *) 
 	| BProd -> if n=1 then "PROD" else "PRODLIST" 
+	| BLetIn -> anomaly "Should be captured before"
       in
       ope(tag,[ast_of_pattern env t;a])
 
-  | PLet (id,a,t,c) ->
-      let c' = ast_of_pattern (add_name (Name id) env) c in
-      ope("LET",[ast_of_pattern env a; 	slam(Some (string_of_id id),c')])
-		
-
   | PCase (typopt,tm,bv) ->
       warning "Old Case syntax";
       ope("MUTCASE",(ast_of_patopt env typopt)