affichage classes et coercions

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

2 files changed, 481 insertions, 405 deletions

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index c482dd15e..61198951d 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -689,18 +689,20 @@ let print_path ((i,j),p) =
      'sTR"] : "; print_class i; 'sTR" >-> ";
      print_class j >]
 
+let _ = Classops.install_path_printer print_path
+
 let print_graph () = 
-  [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >]
+  [< prlist_with_sep pr_fnl print_path (inheritance_graph()) >]
 
 let print_classes () = 
   [< prlist_with_sep pr_spc
        (fun (_,(cl,x)) -> 
           [< 'sTR x.cL_STR  (*; 'sTR(string_of_strength x.cL_STRE) *) >]) 
-       (!cLASSES) >]
+       (classes()) >]
 
 let print_coercions () = 
   [< prlist_with_sep pr_spc
-       (fun (_,(_,v)) -> [< print_coercion_value v >]) (!cOERCIONS) >]
+       (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >]
   
 let cl_of_id id = 
   match string_of_id id with
diff --git a/parsing/termast.ml b/parsing/termast.ml
index aadf51142..d26363ca3 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -21,50 +21,50 @@ open Rawterm
 (* conversion of references                                           *)
 
 let ids_of_ctxt cl =
-  List.map (
-    function 
-	(VAR id) -> id
-      | (Rel n) ->
-	  warning "ids_of_ctxt: rel";
-	  id_of_string ("REL "^(string_of_int n))
-      | _-> anomaly"ids_of_ctxt")
+  List.map
+    (function 
+       | VAR id -> id
+       | Rel n ->
+	   warning "ids_of_ctxt: rel";
+	   id_of_string ("REL "^(string_of_int n))
+       | _-> anomaly"ids_of_ctxt")
     (Array.to_list cl)
 
 let ast_of_ident id = nvar (string_of_id id)
 
 let ast_of_constructor (((sp,tyi),n),ids) =
-   ope("MUTCONSTRUCT",
-       (path_section dummy_loc sp)::(num tyi)::(num n)
-       ::(List.map ast_of_ident ids))
+  ope("MUTCONSTRUCT",
+      (path_section dummy_loc sp)::(num tyi)::(num n)
+      ::(List.map ast_of_ident ids))
 
 let ast_of_mutind ((sp,tyi),ids) =
-   ope("MUTIND",
-       (path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
-
+  ope("MUTIND",
+      (path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
+    
 let ast_of_ref = function
   | RConst (sp,idl) ->
       ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident idl))
   | RAbst (sp) ->
       ope("ABST", (path_section dummy_loc sp)
-	  ::(List.map ast_of_ident (* on triche *) []))
+	    ::(List.map ast_of_ident (* on triche *) []))
   | RInd (ind,idl) -> ast_of_mutind(ind,idl)
   | RConstruct (cstr,idl) -> ast_of_constructor (cstr,idl)
   | RVar id -> nvar (string_of_id id)
-  | REVar (sp,idl) ->
-      ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident idl))
+  | REVar (ev,idl) ->
+      ope("EVAR", (num ev)::(List.map ast_of_ident idl))
   | RMeta n -> ope("META",[num n])
 
 (**********************************************************************)
 (* conversion of patterns                                             *)
 
 let rec ast_of_pattern = function   (* loc is thrown away for printing *)
-    PatVar (loc,Name id) -> nvar (string_of_id id)
+  | PatVar (loc,Name id) -> nvar (string_of_id id)
   | PatVar (loc,Anonymous) -> nvar "_"
   | PatCstr(loc,cstr,args) ->
       ope("PATTCONSTRUCT",
 	  (ast_of_constructor cstr)::List.map ast_of_pattern args)
   | PatAs(loc,id,p) -> ope("PATTAS",[nvar (string_of_id id); ast_of_pattern p])
-
+	
 (* Nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
@@ -96,38 +96,40 @@ type used_idents = identifier list
 
 let occur_id env id0 c =
   let rec occur n = function
-      VAR id             -> id=id0
+    | VAR id             -> id=id0
     | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
     | DOPN (Abst sp,cl)  -> (basename sp = id0) or (array_exists (occur n) cl)
-    | DOPN (MutInd _, cl) as t       -> 
-  (basename (mind_path t) = id0) or (array_exists (occur n) cl)
-| DOPN (MutConstruct _, cl) as t -> 
-    (basename (mind_path t) = id0) or (array_exists (occur n) cl)
-| 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
-| Rel p              ->
-    p>n &
-    (try (fst (lookup_rel (p-n) env) = Name id0)
-     with Not_found -> false) (* Unbound indice : may happen in debug *)
-| DOP0 _             -> false
-  in occur 1 c;;
+    | DOPN (MutInd _, cl) as t -> 
+  	(basename (mind_path t) = id0) or (array_exists (occur n) cl)
+    | DOPN (MutConstruct _, cl) as t -> 
+    	(basename (mind_path t) = id0) or (array_exists (occur n) cl)
+    | 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
+    | Rel p              ->
+    	p>n &
+    	(try (fst (lookup_rel (p-n) env) = Name id0)
+	 with Not_found -> false) (* Unbound indice : may happen in debug *)
+    | DOP0 _             -> false
+  in 
+  occur 1 c
 
 let next_name_not_occuring name l env t =
   let rec next id =
     if List.mem id l or occur_id env id t then next (lift_ident id) else id
-  in match name with
+  in 
+  match name with
     | Name id   -> next id
     | Anonymous -> id_of_string "_"
 
 let concrete_name l env n c =
-  if n = Anonymous then
-    if dependent (Rel 1) c then anomaly "Anonymous should be non dependent"
-    else (None,l)
-  else
+  if n = Anonymous then begin
+    if dependent (Rel 1) c then anomaly "Anonymous should be non dependent";
+    (None,l)
+  end else
     let fresh_id = next_name_not_occuring n l env c in
     let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
     (idopt, fresh_id::l)
@@ -135,7 +137,7 @@ let concrete_name l env n c =
     (* 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
+    | 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 _, cl) as t       -> 
@@ -150,8 +152,8 @@ let global_vars_and_consts t =
     | DLAMV(_,v)         -> Array.fold_left collect acc v
     | _                  -> acc
   in
-  list_uniquize (collect [] t);;
-
+  list_uniquize (collect [] t)
+    
 let used_of = global_vars_and_consts
 let ids_of_env = Sign.ids_of_env
 
@@ -163,34 +165,38 @@ let ids_of_env = Sign.ids_of_env
 
 let indsp_of_id id  =
   let (oper,_) =
-    try let sp = Nametab.sp_of_id CCI id in global_operator sp id
-    with Not_found -> error ("Cannot find reference "^(string_of_id id))
+    try 
+      let sp = Nametab.sp_of_id CCI id in global_operator sp id
+    with Not_found -> 
+      error ("Cannot find reference "^(string_of_id id))
   in
   match oper with
-    MutInd(sp,tyi) -> (sp,tyi)
-  | _ -> errorlabstrm "indsp_of_id" 
-     [< 'sTR ((string_of_id id)^" is not an inductive type") >];;
-
+    | MutInd(sp,tyi) -> (sp,tyi)
+    | _ -> errorlabstrm "indsp_of_id" 
+	  [< 'sTR ((string_of_id id)^" is not an inductive type") >]
+	  
 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
+  | (1, DLAMV(_,cl)) -> cl
   | (n, DLAM (_,c))  -> remove_indtypes (n-1, c)
-  | _                -> anomaly "remove_indtypes: bad list of constructors";;
+  | _                -> 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";;
-
+  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(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
@@ -210,8 +216,7 @@ let isomorphic_to_bool lc =
   let lcparams = Array.map get_params lc in
   Array.length lcparams = 2 & lcparams.(0) = [] & lcparams.(1) = []
 
-let isomorphic_to_tuple lc =
-  Array.length lc = 1
+let isomorphic_to_tuple lc = (Array.length lc = 1)
 
 module PrintingCasesMake =
   functor (Test : sig 
@@ -225,8 +230,8 @@ module PrintingCasesMake =
     type t = section_path * int
     let encode = indsp_of_id
     let check indsp =
-      if not (Test.test (lc_of_lmis (mind_specif_of_mind_light indsp)))
-      then errorlabstrm "check_encode" [< 'sTR Test.error_message >]
+      if not (Test.test (lc_of_lmis (mind_specif_of_mind_light indsp))) then 
+	errorlabstrm "check_encode" [< 'sTR Test.error_message >]
     let decode = sp_of_spi
     let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
@@ -270,7 +275,7 @@ module PrintingLet = Goptions.MakeTable(PrintingCasesLet)
 
 (* Options for printing or not wildcard and synthetisable types *)
 
-open Goptions;;
+open Goptions
 
 let wildcard_value = ref true
 let force_wildcard () = !wildcard_value
@@ -304,51 +309,55 @@ let print_implicits = ref false
 
 (* l est ordonne'ee (croissant), ne garder que les elements <= n *)
 let filter_until n l =
-let rec aux = function
-  [] -> []
- | i::l -> if i > n then []
-                     else i::(aux l)
-in aux l;;
+  let rec aux = function
+    | [] -> []
+    | i::l -> if i > n then [] else i::(aux l)
+  in 
+  aux l
 
 (* l est ordonne'e (de'croissant), n>=max(l), diviser l en deux listes,
    la 2eme est la plus longue se'quence commencant par n,
    la 1ere contient les autres elements *)
 
 let rec div_implicits n = 
- function [] -> [],[]
-        | i::l -> if i = n then let l1,l2=(div_implicits (n-1) l) in l1,i::l2
-                           else i::l,[];;
+  function 
+    | [] -> [],[]
+    | i::l -> 
+	if i = n then 
+	  let l1,l2=(div_implicits (n-1) l) in l1,i::l2
+        else 
+	  i::l,[]
 
 let bdize_app c al =
   let impl =
     match c with
-        DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp
+      | DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp
       | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp
       | DOPN(Const sp,_) -> constant_implicits_list sp
       | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
       | _ -> []
   in
-    if impl = []
-    then ope("APPLIST", al)
-    else if !print_implicits
-    then ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al)
-    else 
-      let largs = List.length al - 1 in
-      let impl = List.rev (filter_until largs impl) in
-      let impl1,impl2=div_implicits largs impl in
-      let al1 = Array.of_list al in
-        List.iter
-          (fun i -> al1.(i) <-
-             ope("XTRA", [str "!"; str "EX"; num i; al1.(i)]))
-          impl2;
-        List.iter
-          (fun i -> al1.(i) <-
-             ope("XTRA",[str "!"; num i; al1.(i)]))
-          impl1;
-        al1.(0) <- ope("XTRA",[str "!"; al1.(0)]);
-        ope("APPLIST",Array.to_list al1)
-
-type optioncast = WithCast | WithoutCast;;
+  if impl = [] then 
+    ope("APPLIST", al)
+  else if !print_implicits then 
+    ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al)
+  else 
+    let largs = List.length al - 1 in
+    let impl = List.rev (filter_until largs impl) in
+    let impl1,impl2=div_implicits largs impl in
+    let al1 = Array.of_list al in
+    List.iter
+      (fun i -> al1.(i) <-
+         ope("XTRA", [str "!"; str "EX"; num i; al1.(i)]))
+      impl2;
+    List.iter
+      (fun i -> al1.(i) <-
+         ope("XTRA",[str "!"; num i; al1.(i)]))
+      impl1;
+    al1.(0) <- ope("XTRA",[str "!"; al1.(0)]);
+    ope("APPLIST",Array.to_list al1)
+
+type optioncast = WithCast | WithoutCast
 
 (* [reference_tree p] pre-computes the variables and de bruijn occurring
    in a term to avoid a O(n2) factor when computing dependent each time *)
@@ -365,7 +374,7 @@ let combine l =
   NODE (combine_rec l,l)
 
 let rec reference_tree p = function
-    VAR id -> NODE (([],[id]),[])
+  | VAR id -> NODE (([],[id]),[])
   | Rel n  -> NODE (([n-p],[]),[])
   | DOP0 op -> NODE (([],[]),[])
   | DOP1(op,c) -> reference_tree p c
@@ -396,167 +405,197 @@ let computable p k =
        engendrera un prédicat non dépendant) *)
 
   let rec striprec = function
-      (0,DOP2(Lambda,_,DLAM(_,d))) -> false
+    | (0,DOP2(Lambda,_,DLAM(_,d))) -> false
     | (0,d               )         -> noccur_bet 1 k d
     | (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
     |  _                           -> false
-  in striprec (k,p)
+  in 
+  striprec (k,p)
 
 (* Main translation function from constr -> ast *)
 
 let old_bdize_depcast opcast at_top env t =
   let init_avoid = if at_top then ids_of_env env else [] in
-  let rec bdrec avoid env t = 
-    match collapse_appl t with
-
-  (* Not well-formed constructions *)
-  | DLAM(na,c) ->
-      (match concrete_name avoid env na c with
-          (Some id,avoid') -> slam(Some (string_of_id id),
-                                   bdrec avoid' (add_rel (Name id,()) env) c)
-        | (None,avoid')    -> slam(None,bdrec avoid' env (pop c)))
-  | DLAMV(na,cl) ->
-    if not(array_exists (dependent (Rel 1)) cl) then
-      slam(None,ope("V$",array_map_to_list
-		      (fun c -> bdrec avoid env (pop c)) cl))
-    else
-      let id = next_name_away na avoid
-      in slam(Some (string_of_id id),
-              ope("V$", array_map_to_list
-		    (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
-
-  (* Well-formed constructions *)
-  | regular_constr -> 
-  (match kind_of_term regular_constr with
-  | IsRel n ->
-      (try match fst(lookup_rel n env) with
-           Name id   -> nvar (string_of_id id)
-         | Anonymous -> raise Not_found
-       with Not_found -> ope("REL",[num n]))
-      (* TODO: Change this to subtract the current depth *)
-  | IsMeta n -> ope("META",[num n])
-  | IsVar id -> nvar (string_of_id id)
-  | IsXtra s -> ope("XTRA",[str s])
-  | IsSort s ->
-      (match s with
-	 | Prop Null -> ope("PROP",[])
-	 | Prop Pos -> ope("SET",[])
-	 | Type u -> ope("TYPE",[path_section dummy_loc u.u_sp; num u.u_num]))
-  | IsCast (c1,c2) ->
-      if opcast=WithoutCast 
-      then bdrec avoid env c1 
-      else ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
-  | IsProd (Anonymous,ty,c) ->
-      (* Anonymous product are never factorized *)
-	ope("PROD",[bdrec [] env ty;slam(None,bdrec avoid env (pop c))])
-  | IsProd (Name _ as na,ty,c) ->
-      let (n,a) = factorize_binder 1 avoid env Prod na ty c in
-         (* PROD et PRODLIST doivent être distingués à cause du cas
-	    non dépendant, pour isoler l'implication; peut-être un constructeur
-	    ARROW serait-il plus justifié ? *)
-      let oper = if n=1 then "PROD" else "PRODLIST" in
-	ope(oper,[bdrec [] env ty;a])
-  | IsLambda (na,ty,c) ->
-      let (_,a) = factorize_binder 1 avoid env Lambda na ty c in
-         (* LAMBDA et LAMBDALIST se comportent pareil *)
-	ope("LAMBDALIST",[bdrec [] env ty;a])
-  | IsAppL (f,args) ->
-      bdize_app f (List.map (bdrec avoid env) (f::args))
-
-  | IsConst (sp,cl) ->
-      ope("CONST",((path_section dummy_loc sp)::
-		   (array_map_to_list (bdrec avoid env) cl)))
-  | IsAbst (sp,cl) ->
-      ope("ABST",((path_section dummy_loc sp)::
-		   (array_map_to_list (bdrec avoid env) cl)))
-  | IsMutInd (sp,tyi,cl) ->
-      ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
-		   (array_map_to_list (bdrec avoid env) cl)))
-  | IsMutConstruct (sp,tyi,n,cl) ->
-      ope("MUTCONSTRUCT",((path_section dummy_loc sp)::(num tyi)::(num n)::
-		   (array_map_to_list (bdrec avoid env) cl)))
-  | IsMutCase (annot,p,c,bl) ->
-      let synth_type       = synthetize_type () in
-      let tomatch = bdrec avoid env c in
-	begin match annot with
-            None -> (* Pas d'annotation --> affichage avec vieux Case *)
-              let pred = bdrec avoid env p in
-              let bl' = array_map_to_list (bdrec avoid env) bl in
-		ope("MUTCASE",pred::tomatch::bl')
-	  | Some indsp ->
-              let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
-              let lc = lc_of_lmis lmis in
-              let lcparams = Array.map get_params lc in
-              let k = (nb_prod mip.mind_arity.body) - mib.mind_nparams in
-              let pred = if synth_type & computable p k & lcparams <> [||]
-              then (str "SYNTH")
-              else bdrec avoid env p in
-		if PrintingIf.active indsp
-		then ope("FORCEIF", [ pred; tomatch;
-                                      bdrec avoid env bl.(0); 
-                                      bdrec avoid env bl.(1) ])
-		else
-		  let idconstructs = mip.mind_consnames in
-		  let asttomatch = ope("TOMATCH", [tomatch]) in
-		  let eqnv =
-		    array_map3 (bdize_eqn avoid env) idconstructs
-		      lcparams bl in
-		  let eqnl = Array.to_list eqnv in
-		  let tag =
-		    if PrintingLet.active indsp then "FORCELET" else "MULTCASE"
-		  in ope(tag,pred::asttomatch::eqnl)
-	end
-
-  | IsFix (nv,n,cl,lfn,vt) ->
-      let lfi = List.map (fun na -> next_name_away na avoid) lfn in
-      let def_env = List.fold_left
-                      (fun env id -> add_rel (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 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_rel (Name id,()) env in
-              split_lambda (ast_of_bind::binds) 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 ast = bdrec avoid env t in
-	    let id = next_name_away na avoid in
-            let new_env = add_rel (Name id,()) env in
-	      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
-	     let ast_of_typ = split_product env avoid (nv.(i)+1,cl.(i)) in
-               ope("FDECL",
-                   [nvar (string_of_id fi); ope ("BINDERS",List.rev lparams);
-		    ast_of_typ; ast_of_def ]))
-          0 lfi 
-      in ope("FIX", (nvar (string_of_id f))::listdecl)
-
-  | IsCoFix (n,cl,lfn,vt) ->
-      let lfi = List.map (fun na -> next_name_away na avoid) lfn in
-      let def_env =
-	List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in
-      let def_avoid = lfi@avoid in
-      let f = List.nth lfi n in
-      let listdecl =
-        list_map_i (fun i fi -> ope("CFDECL",
-                               [nvar (string_of_id fi);
-				bdrec avoid env cl.(i);
-                                bdrec def_avoid def_env vt.(i)]))
-          0 lfi
-      in ope("COFIX", (nvar (string_of_id f))::listdecl))
+  let rec bdrec avoid env t = match collapse_appl t with
+    (* Not well-formed constructions *)
+    | DLAM(na,c) ->
+	(match concrete_name avoid env na c with
+           | (Some id,avoid') -> 
+	       slam(Some (string_of_id id),
+                    bdrec avoid' (add_rel (Name id,()) env) c)
+           | (None,avoid') -> 
+	       slam(None,bdrec avoid' env (pop c)))
+    | DLAMV(na,cl) ->
+	if not(array_exists (dependent (Rel 1)) cl) then
+	  slam(None,ope("V$",array_map_to_list
+			  (fun c -> bdrec avoid env (pop c)) cl))
+	else
+	  let id = next_name_away na avoid in 
+	  slam(Some (string_of_id id),
+	       ope("V$", array_map_to_list
+		     (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
+	    
+    (* Well-formed constructions *)
+    | regular_constr -> 
+	(match kind_of_term regular_constr with
+	   | IsRel n ->
+	       (try 
+		  match fst(lookup_rel n env) with
+		    | Name id   -> nvar (string_of_id id)
+		    | Anonymous -> raise Not_found
+		with Not_found -> 
+		  ope("REL",[num n]))
+	     (* TODO: Change this to subtract the current depth *)
+	   | IsMeta n -> ope("META",[num n])
+	   | IsVar id -> nvar (string_of_id id)
+	   | IsXtra s -> ope("XTRA",[str s])
+	   | IsSort s ->
+	       (match s with
+		  | Prop Null -> ope("PROP",[])
+		  | Prop Pos -> ope("SET",[])
+		  | Type u -> 
+		      ope("TYPE",
+			  [path_section dummy_loc u.u_sp; num u.u_num]))
+	   | IsCast (c1,c2) ->
+	       if opcast=WithoutCast then 
+		 bdrec avoid env c1 
+	       else 
+		 ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
+	   | IsProd (Anonymous,ty,c) ->
+                    (* Anonymous product are never factorized *)
+	       ope("PROD",[bdrec [] env ty;
+			   slam(None,bdrec avoid env (pop c))])
+	   | IsProd (Name _ as na,ty,c) ->
+	       let (n,a) = factorize_binder 1 avoid env Prod na ty c in
+               (* PROD et PRODLIST doivent être distingués à cause du cas
+                  non dépendant, pour isoler l'implication; peut-être 
+	          un constructeur ARROW serait-il plus justifié ? *)
+	       let oper = if n=1 then "PROD" else "PRODLIST" in
+	       ope(oper,[bdrec [] env ty;a])
+	   | IsLambda (na,ty,c) ->
+	       let (_,a) = factorize_binder 1 avoid env Lambda na ty c in
+               (* LAMBDA et LAMBDALIST se comportent pareil *)
+	       ope("LAMBDALIST",[bdrec [] env ty;a])
+	   | IsAppL (f,args) ->
+	       bdize_app f (List.map (bdrec avoid env) (f::args))
+	   | IsConst (sp,cl) ->
+	       ope("CONST",((path_section dummy_loc sp)::
+			    (array_map_to_list (bdrec avoid env) cl)))
+	   | IsEvar (ev,cl) ->
+	       ope("EVAR",((num ev)::
+			   (array_map_to_list (bdrec avoid env) cl)))
+	   | IsAbst (sp,cl) ->
+	       ope("ABST",((path_section dummy_loc sp)::
+			   (array_map_to_list (bdrec avoid env) cl)))
+	   | IsMutInd (sp,tyi,cl) ->
+	       ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
+			     (array_map_to_list (bdrec avoid env) cl)))
+	   | IsMutConstruct (sp,tyi,n,cl) ->
+	       ope("MUTCONSTRUCT",
+		   ((path_section dummy_loc sp)::(num tyi)::(num n)::
+		    (array_map_to_list (bdrec avoid env) cl)))
+	   | IsMutCase (annot,p,c,bl) ->
+	       let synth_type = synthetize_type () in
+	       let tomatch = bdrec avoid env c in
+	       begin match annot with
+		 | None -> 
+	             (* Pas d'annotation --> affichage avec vieux Case *)
+		     let pred = bdrec avoid env p in
+		     let bl' = array_map_to_list (bdrec avoid env) bl in
+		     ope("MUTCASE",pred::tomatch::bl')
+		 | Some indsp ->
+		     let (mib,mip as lmis) = 
+		       mind_specif_of_mind_light indsp in
+		     let lc = lc_of_lmis lmis in
+		     let lcparams = Array.map get_params lc in
+		     let k = (nb_prod mip.mind_arity.body) - 
+			     mib.mind_nparams in
+		     let pred = 
+		       if synth_type & computable p k & lcparams <> [||] then
+			 (str "SYNTH")
+		       else 
+			 bdrec avoid env p 
+		     in
+		     if PrintingIf.active indsp then 
+		       ope("FORCEIF", [ pred; tomatch;
+					bdrec avoid env bl.(0); 
+					bdrec avoid env bl.(1) ])
+		     else
+		       let idconstructs = mip.mind_consnames in
+		       let asttomatch = ope("TOMATCH", [tomatch]) in
+		       let eqnv =
+			 array_map3 (bdize_eqn avoid env) idconstructs
+			   lcparams bl in
+		       let eqnl = Array.to_list eqnv in
+		       let tag =
+			 if PrintingLet.active indsp then 
+			   "FORCELET" 
+			 else 
+			   "MULTCASE"
+		       in 
+		       ope(tag,pred::asttomatch::eqnl)
+	       end
+	       
+	   | IsFix (nv,n,cl,lfn,vt) ->
+	       let lfi = List.map (fun na -> next_name_away na avoid) lfn in
+	       let def_env = 
+		 List.fold_left
+		   (fun env id -> add_rel (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 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_rel (Name id,()) env in
+		     split_lambda (ast_of_bind::binds) 
+		       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 ast = bdrec avoid env t in
+		     let id = next_name_away na avoid in
+		     let new_env = add_rel (Name id,()) env in
+		     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
+		      let ast_of_typ = 
+			split_product env avoid (nv.(i)+1,cl.(i)) in
+		      ope("FDECL",
+			  [nvar (string_of_id fi); 
+			   ope ("BINDERS",List.rev lparams);
+			   ast_of_typ; ast_of_def ]))
+		   0 lfi 
+	       in 
+	       ope("FIX", (nvar (string_of_id f))::listdecl)
+
+	   | IsCoFix (n,cl,lfn,vt) ->
+	       let lfi = List.map (fun na -> next_name_away na avoid) lfn in
+	       let def_env =
+		 List.fold_left 
+		   (fun env id -> add_rel (Name id,()) env) env lfi in
+	       let def_avoid = lfi@avoid in
+	       let f = List.nth lfi n in
+	       let listdecl =
+		 list_map_i (fun i fi -> ope("CFDECL",
+					     [nvar (string_of_id fi);
+					      bdrec avoid env cl.(i);
+					      bdrec def_avoid def_env vt.(i)]))
+		   0 lfi
+	       in 
+	       ope("COFIX", (nvar (string_of_id f))::listdecl))
 
   and bdize_eqn avoid env constructid construct_params branch =
     let print_underscore = force_wildcard () in
@@ -642,95 +681,121 @@ variables of a goal.
 
 (* $Id$ *)
 
-exception StillDLAM;;
+exception StillDLAM
 
 let rec detype t = 
   match collapse_appl t with
-      (* Not well-formed constructions *)
+    (* Not well-formed constructions *)
     | DLAM _ | DLAMV _ -> raise StillDLAM
-	  (* Well-formed constructions *)
+    (* Well-formed constructions *)
     | regular_constr -> 
-  (match kind_of_term regular_constr with
-  | IsRel n -> RRel (dummy_loc,n)
-  | IsMeta n -> RRef (dummy_loc,RMeta n)
-  | IsVar id -> RRef (dummy_loc,RVar id)
-  | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr"
-    (*       ope("XTRA",((str s):: pl@(List.map detype cl)))*)
-  | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
-  | IsSort (Type _) -> RSort (dummy_loc,RType)
-  | IsCast (c1,c2) -> RCast(dummy_loc,detype c1,detype c2)
-  | IsProd (na,ty,c) -> RBinder (dummy_loc,BProd,na,detype ty,detype c)
-  | IsLambda (na,ty,c) -> RBinder (dummy_loc,BLambda,na,detype ty,detype c)
-  | IsAppL (f,args) -> RApp (dummy_loc,detype f,List.map detype args)
-  | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl))
-  | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr"
-  | IsMutInd (sp,tyi,cl) ->  RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl))
-  | IsMutConstruct (sp,tyi,n,cl) -> 
-      RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl))
-  | IsMutCase (annot,p,c,bl) ->
-      let synth_type = synthetize_type () in
-      let tomatch = detype c in
-	begin match annot with
-            None -> (* Pas d'annotation --> affichage avec vieux Case *)
-              warning "Printing in old Case syntax";
-              ROldCase (dummy_loc,false,Some (detype p),
-			tomatch,Array.map detype bl)
-	  | Some indsp ->
-              let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
-              let lc = lc_of_lmis lmis in
-              let lcparams = Array.map get_params lc in
-	      let k = (nb_prod mip.mind_arity.body) - mib.mind_nparams in
-              let pred = if synth_type & computable p k & lcparams <> [||]
-              then None
-              else Some (detype p) in
-	      let constructs = 
-		Array.init
-		  (Array.length mip.mind_consnames)
-		  (fun i -> ((indsp,i),[] (* on triche *))) in
-	      let eqnv = array_map3 bdize_eqn constructs lcparams bl in
-	      let eqnl = Array.to_list eqnv in
-	      let tag =
-		if PrintingLet.active indsp then PrintLet else
-		if PrintingIf.active indsp then PrintIf else PrintCases
-	      in RCases (dummy_loc,tag,pred,[tomatch],eqnl)
-	end
-
-  | IsFix (nv,n,cl,lfn,vt) ->
-      let l = Array.of_list (List.map
-	       (function Name id -> id | Anonymous -> anomaly"detype") lfn) in
-      RRec(dummy_loc,RFix (nv,n),l,Array.map detype cl,Array.map detype vt)
-  | IsCoFix (n,cl,lfn,vt) ->
-      let l = Array.of_list (List.map
-	       (function Name id -> id | Anonymous -> anomaly"detype") lfn) in
-      RRec(dummy_loc,RCofix n,l,Array.map detype cl,Array.map detype vt))
-
-  and bdize_eqn constr_id construct_params branch =
-   let avoid = global_vars_and_consts branch in
-   let make_pat x avoid b =
-     if not (force_wildcard ()) or (dependent (Rel 1) b) then
-       let id = next_name_away x avoid in
-       (PatVar (dummy_loc,Name id)),id::avoid,id
-     else PatVar (dummy_loc,Anonymous),avoid,id_of_string "_" in
-   let rec buildrec idl patlist avoid = function
-
-	_::l, DOP2(Lambda,_,DLAM(x,b))
-	-> let pat,new_avoid,id = make_pat x avoid b in
-        buildrec (id::idl) (pat::patlist) new_avoid (l,b)
+  	(match kind_of_term regular_constr with
+	   | IsRel n -> RRel (dummy_loc,n)
+	   | IsMeta n -> RRef (dummy_loc,RMeta n)
+	   | IsVar id -> RRef (dummy_loc,RVar id)
+	   | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr"
+	     (*       ope("XTRA",((str s):: pl@(List.map detype cl)))*)
+	   | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
+	   | IsSort (Type _) -> RSort (dummy_loc,RType)
+	   | IsCast (c1,c2) -> RCast(dummy_loc,detype c1,detype c2)
+	   | IsProd (na,ty,c) -> 
+	       RBinder (dummy_loc,BProd,na,detype ty,detype c)
+	   | IsLambda (na,ty,c) -> 
+	       RBinder (dummy_loc,BLambda,na,detype ty,detype c)
+	   | IsAppL (f,args) -> RApp (dummy_loc,detype f,List.map detype args)
+	   | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl))
+	   | IsEvar (ev,cl) -> RRef (dummy_loc,REVar (ev,ids_of_ctxt cl))
+	   | IsAbst (sp,cl) -> 
+	       anomaly "bdize: Abst should no longer occur in constr"
+	   | IsMutInd (sp,tyi,cl) ->
+	       RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl))
+	   | IsMutConstruct (sp,tyi,n,cl) -> 
+	       RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl))
+	   | IsMutCase (annot,p,c,bl) ->
+	       let synth_type = synthetize_type () in
+	       let tomatch = detype c in
+	       begin match annot with
+		 | None -> (* Pas d'annotation --> affichage avec vieux Case *)
+		     warning "Printing in old Case syntax";
+		     ROldCase (dummy_loc,false,Some (detype p),
+			       tomatch,Array.map detype bl)
+		 | Some indsp ->
+		     let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
+		     let lc = lc_of_lmis lmis in
+		     let lcparams = Array.map get_params lc in
+		     let k = (nb_prod mip.mind_arity.body) - 
+			     mib.mind_nparams in
+		     let pred = 
+		       if synth_type & computable p k & lcparams <> [||] then
+			 None
+		       else 
+			 Some (detype p) 
+		     in
+		     let constructs = 
+		       Array.init
+			 (Array.length mip.mind_consnames)
+			 (fun i -> ((indsp,i),[] (* on triche *))) in
+		     let eqnv = array_map3 bdize_eqn constructs lcparams bl in
+		     let eqnl = Array.to_list eqnv in
+		     let tag =
+		       if PrintingLet.active indsp then 
+			 PrintLet 
+		       else if PrintingIf.active indsp then 
+			 PrintIf 
+		       else 
+			 PrintCases
+		     in 
+		     RCases (dummy_loc,tag,pred,[tomatch],eqnl)
+	       end
 	       
-      | l   , DOP2(Cast,b,_)     (* Oui, il y a parfois des cast *)
-	-> buildrec idl patlist avoid (l,b)
+	   | IsFix (nv,n,cl,lfn,vt) ->
+	       let l = 
+		 Array.of_list 
+		   (List.map
+		      (function Name id -> id | Anonymous -> anomaly"detype")
+		      lfn) 
+	       in
+	       RRec(dummy_loc,RFix (nv,n),l,Array.map detype cl,
+		    Array.map detype vt)
+	   | IsCoFix (n,cl,lfn,vt) ->
+	       let l = 
+		 Array.of_list 
+		   (List.map
+		      (function Name id -> id | Anonymous -> anomaly"detype")
+		      lfn) 
+	       in
+	       RRec(dummy_loc,RCofix n,l,Array.map detype cl,
+		    Array.map detype vt))
+	
+and bdize_eqn constr_id construct_params branch =
+  let avoid = global_vars_and_consts branch in
+  let make_pat x avoid b =
+    if not (force_wildcard ()) or (dependent (Rel 1) b) then
+      let id = next_name_away x avoid in
+      (PatVar (dummy_loc,Name id)),id::avoid,id
+    else 
+      PatVar (dummy_loc,Anonymous),avoid,id_of_string "_" 
+  in
+  let rec buildrec idl patlist avoid = function
+    | _::l, DOP2(Lambda,_,DLAM(x,b)) -> 
+	let pat,new_avoid,id = make_pat x avoid b in
+        buildrec (id::idl) (pat::patlist) new_avoid (l,b)
 	  
-      | x::l, b (* eta-expansion : n'arrivera plus lorsque tous les
+    | l   , DOP2(Cast,b,_) ->    (* Oui, il y a parfois des cast *)
+	buildrec idl patlist avoid (l,b)
+	  
+    | x::l, b -> (* eta-expansion : n'arrivera plus lorsque tous les
                    termes seront construits à partir de la syntaxe Cases *)
-	-> (* nommage de la nouvelle variable *)
-	   let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
-           let pat,new_avoid,id = make_pat x avoid new_b in
-	   buildrec (id::idl) (pat::patlist) new_avoid (l,new_b)
+	(* nommage de la nouvelle variable *)
+	let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
+        let pat,new_avoid,id = make_pat x avoid new_b in
+	buildrec (id::idl) (pat::patlist) new_avoid (l,new_b)
+	  
+    | []  , rhs	-> 
+	(idl, [PatCstr(dummy_loc, constr_id, List.rev patlist)], detype rhs)
+  in 
+  buildrec [] [] avoid (construct_params,branch)
 
-      | []  , rhs
-	-> (idl, [PatCstr(dummy_loc, constr_id, List.rev patlist)], detype rhs)
-    in buildrec [] [] avoid (construct_params,branch)
-;;
 
 let implicit_of_ref = function
   | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
@@ -740,10 +805,10 @@ let implicit_of_ref = function
   | _ -> []
 
 let ast_of_app impl f args =
-  if impl = []
-  then ope("APPLIST", f::args)
-  else if !print_implicits
-  then ope("APPLISTEXPL", (f::args))
+  if impl = [] then 
+    ope("APPLIST", f::args)
+  else if !print_implicits then 
+    ope("APPLISTEXPL", (f::args))
   else 
     let largs = List.length args in
     let impl = List.rev (filter_until largs impl) in
@@ -764,16 +829,16 @@ let rec ast_of_raw avoid env = function
   | RRef (_,ref) -> ast_of_ref ref
   | RRel (_,n) ->
       (try match fst (lookup_rel n env) with
-	    Name id   -> ast_of_ident id
-	  | Anonymous -> 
-	      anomaly "ast_of_raw: index to an anonymous variable"
-	with Not_found ->
-	  ope("REL",[num (n - List.length (get_rels env))]))
+	 | Name id   -> ast_of_ident id
+	 | Anonymous -> 
+	     anomaly "ast_of_raw: index to an anonymous variable"
+       with Not_found ->
+	 ope("REL",[num (n - List.length (get_rels env))]))
   | RApp (_,f,args) ->
       let astf = ast_of_raw avoid env  f in
       let astargs = List.map (ast_of_raw avoid env ) args in
       (match f with 
-	   RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
+	 | RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
 	 | _           -> ast_of_app [] astf astargs)
   | RBinder (_,BProd,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
@@ -783,28 +848,30 @@ let rec ast_of_raw avoid env = function
       let (n,a) = factorize_binder 1 avoid env bk na t c in
       let tag = match bk with
 	  (* LAMBDA et LAMBDALIST se comportent pareil *)
-	  BLambda -> "LAMBDALIST"
+	| BLambda -> "LAMBDALIST"
 	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
 	  (* non dépendant, pour isoler l'implication; peut-être un *)
 	  (* constructeur ARROW serait-il plus justifié ? *) 
-	| BProd -> if n=1 then "PROD" else "PROLIST" in
+	| BProd -> if n=1 then "PROD" else "PROLIST" 
+      in
       ope(tag,[ast_of_raw [] env t;a])
 
   | RCases (_,printinfo,typopt,tml,eqns) ->
       let pred = ast_of_rawopt avoid env typopt in
       let tag = match printinfo with
-	  PrintIf -> "FORCEIF"
+	| PrintIf -> "FORCEIF"
 	| PrintLet -> "FORCELET"
-	| PrintCases -> "MULTCASE" in
+	| PrintCases -> "MULTCASE" 
+      in
       let asttomatch = ope("TOMATCH", List.map (ast_of_raw avoid env) tml) in
-      let asteqns = List.map (ast_of_eqn avoid env) eqns
-      in ope(tag,pred::asttomatch::asteqns)
-
+      let asteqns = List.map (ast_of_eqn avoid env) eqns in 
+      ope(tag,pred::asttomatch::asteqns)
+	
   | ROldCase (_,isrec,typopt,tm,bv) ->
       warning "Old Case syntax";
       ope("MUTCASE",(ast_of_rawopt avoid env typopt)
-	  ::(ast_of_raw avoid env tm)
-	  ::(Array.to_list (Array.map (ast_of_raw avoid env) bv)))
+	    ::(ast_of_raw avoid env tm)
+	    ::(Array.to_list (Array.map (ast_of_raw avoid env) bv)))
   | RRec (_,fk,idv,tyv,bv) ->
       let lfi = Array.map (fun id -> next_ident_away id avoid) idv in
       let alfi = Array.map ast_of_ident lfi in
@@ -813,40 +880,46 @@ let rec ast_of_raw avoid env = function
 	List.fold_left (fun env id -> add_rel (Name id,()) env) env 
 	  (Array.to_list lfi) in
       (match fk with 
-	| RFix (nv,n) ->
-            let rec split_lambda binds avoid env = function
-		(0, t) -> (binds,ast_of_raw avoid env t)
-	      | (n, RBinder(_,BLambda,na,t,b)) ->
-		  let ast = ast_of_raw avoid env t in
-		  let id = next_name_away na avoid in
-		  let bind = ope("BINDER",[ast;ast_of_ident id]) in
-		  split_lambda (bind::binds) (id::avoid)
-		    (add_rel (na,()) env) (n-1,b)
-	      | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
-	    let rec split_product avoid env = function
-		(0, t) -> ast_of_raw avoid env t
-	      | (n, RBinder(_,BProd,na,t,b)) ->
-		  let id = next_name_away na avoid in
-		  split_product (id::avoid) (add_rel (na,()) env) (n-1,b)
-	      | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
-	    let listdecl = 
-	      Array.mapi
-		(fun i fi ->
-		   let (lparams,astdef) =
-		     split_lambda [] avoid def_env (nv.(i)+1,bv.(i)) in
-		   let asttyp = split_product avoid env (nv.(i)+1,tyv.(i)) in
-		   ope("FDECL",
-		       [fi; ope ("BINDERS",List.rev lparams); asttyp; astdef]))
-		alfi
-	    in ope("FIX", alfi.(n)::(Array.to_list listdecl))
-	| RCofix n -> 
-	    let listdecl =
-              Array.mapi (fun i fi -> ope("CFDECL",
-				     [fi;
-				      ast_of_raw avoid env tyv.(i);
-                                      ast_of_raw def_avoid def_env bv.(i)]))
-		alfi
-	    in ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
+	 | RFix (nv,n) ->
+             let rec split_lambda binds avoid env = function
+	       | (0, t) -> (binds,ast_of_raw avoid env t)
+	       | (n, RBinder(_,BLambda,na,t,b)) ->
+		   let ast = ast_of_raw avoid env t in
+		   let id = next_name_away na avoid in
+		   let bind = ope("BINDER",[ast;ast_of_ident id]) in
+		   split_lambda (bind::binds) (id::avoid)
+		     (add_rel (na,()) env) (n-1,b)
+	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" 
+	     in
+	     let rec split_product avoid env = function
+	       | (0, t) -> ast_of_raw avoid env t
+	       | (n, RBinder(_,BProd,na,t,b)) ->
+		   let id = next_name_away na avoid in
+		   split_product (id::avoid) (add_rel (na,()) env) (n-1,b)
+	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" 
+	     in
+	     let listdecl = 
+	       Array.mapi
+		 (fun i fi ->
+		    let (lparams,astdef) =
+		      split_lambda [] avoid def_env (nv.(i)+1,bv.(i)) in
+		    let asttyp = split_product avoid env (nv.(i)+1,tyv.(i)) in
+		    ope("FDECL",
+		       	[fi; ope ("BINDERS",List.rev lparams); 
+			 asttyp; astdef]))
+		 alfi
+	     in 
+	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
+	 | RCofix n -> 
+	     let listdecl =
+               Array.mapi 
+		 (fun i fi -> ope("CFDECL",
+				  [fi;
+				   ast_of_raw avoid env tyv.(i);
+				   ast_of_raw def_avoid def_env bv.(i)]))
+		 alfi
+	     in 
+	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
 
   | RSort (_,s) ->
       (match s with
@@ -856,7 +929,7 @@ let rec ast_of_raw avoid env = function
   | RHole _ -> ope("ISEVAR",[])
   | RCast (_,c,t) ->
       ope("CAST",[ast_of_raw avoid env c;ast_of_raw avoid env t])
-
+	
 and ast_of_eqn avoid env (idl,pl,c) =
   let new_env = 
     List.fold_left (fun env id -> add_rel (Name id,()) env) env idl in
@@ -866,50 +939,51 @@ and ast_of_eqn avoid env (idl,pl,c) =
 and ast_of_rawopt avoid env  = function
   | None -> (str "SYNTH")
   | Some p -> ast_of_raw avoid env  p
-
+	
 and factorize_binder n avoid env  oper na ty c =
   let (env2, avoid2,na2) =
     match weak_concrete_name avoid env na c with
-	(Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) 
+      | (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) 
       | (None,l')    -> add_rel (Anonymous,()) env, l', None
   in
   let (p,body) = match c with
       RBinder(_,oper',na',ty',c')
 	when (oper = oper')
 	  & (ast_of_raw avoid env ty) 
-	    = (ast_of_raw avoid (add_rel (na,()) env) ty')
-	  & not (na' = Anonymous & oper = BProd)
-	  -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
+	  = (ast_of_raw avoid (add_rel (na,()) env) ty')
+	    & not (na' = Anonymous & oper = BProd)
+	    -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
     | _ -> (n,ast_of_raw avoid2 env2 c)
-  in (p,slam(na2, body))
-
+  in 
+  (p,slam(na2, body))
+       
 (* A brancher sur le vrai concrete_name *)
 and weak_concrete_name avoid env na c =
   match na with
-      Anonymous -> (None,avoid)
+    | Anonymous -> (None,avoid)
     | Name id -> (Some id,avoid)
-;;
 
 let bdize_no_casts at_top env t =
   try
     let avoid = if at_top then ids_of_env env else [] in
     ast_of_raw avoid env (detype t)
-  with StillDLAM -> old_bdize_depcast WithoutCast at_top env t
+  with StillDLAM -> 
+    old_bdize_depcast WithoutCast at_top env t
 
 (* En attendant que strong aille dans term.ml *)
 let rec strong whdfun t = 
   match whdfun t with 
-    DOP0 _ as t -> t
+    | DOP0 _ as t -> t
 	(* Cas ad hoc *)
-  | DOP1(oper,c) -> DOP1(oper,strong whdfun c)
-  | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2)
-  | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl)
-  | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl)
-  | DLAM(na,c) -> DLAM(na,strong whdfun c)
-  | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c)
-  | VAR _ as t -> t
-  | Rel _ as t -> t
+    | DOP1(oper,c) -> DOP1(oper,strong whdfun c)
+    | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2)
+    | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl)
+    | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl)
+    | DLAM(na,c) -> DLAM(na,strong whdfun c)
+    | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c)
+    | VAR _ as t -> t
+    | Rel _ as t -> t
 
 let bdize at_top env t = bdize_no_casts at_top env (strong strip_outer_cast t) 
-
+			   
 let ast_of_rawconstr = ast_of_raw []