module Termast

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

8 files changed, 110 insertions, 55 deletions

diff --git a/.depend b/.depend
index b27a5cafc..c1c5800df 100644
--- a/.depend
+++ b/.depend
@@ -38,7 +38,8 @@ library/declare.cmi: kernel/constant.cmi kernel/inductive.cmi \
 library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/typing.cmi kernel/univ.cmi 
-library/impargs.cmi: kernel/names.cmi 
+library/goptions.cmi: kernel/names.cmi 
+library/impargs.cmi: kernel/names.cmi kernel/term.cmi 
 library/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/term.cmi 
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
@@ -47,7 +48,8 @@ library/library.cmi: lib/pp.cmi
 library/nametab.cmi: kernel/names.cmi 
 library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
-parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
+parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
+    parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: kernel/evd.cmi kernel/names.cmi pretyping/rawterm.cmi \
     kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
@@ -283,6 +285,10 @@ library/global.cmx: kernel/environ.cmx kernel/generic.cmx \
     kernel/inductive.cmx kernel/instantiate.cmx kernel/sign.cmx \
     library/summary.cmx kernel/term.cmx kernel/typing.cmx lib/util.cmx \
     library/global.cmi 
+library/goptions.cmo: library/lib.cmi library/libobject.cmi kernel/names.cmi \
+    lib/pp.cmi library/summary.cmi lib/util.cmi library/goptions.cmi 
+library/goptions.cmx: library/lib.cmx library/libobject.cmx kernel/names.cmx \
+    lib/pp.cmx library/summary.cmx lib/util.cmx library/goptions.cmi 
 library/impargs.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi kernel/inductive.cmi kernel/names.cmi \
     kernel/reduction.cmi library/summary.cmi kernel/term.cmi \
@@ -361,12 +367,16 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
     parsing/printer.cmi 
-parsing/termast.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
-    kernel/generic.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    lib/pp.cmi kernel/term.cmi lib/util.cmi parsing/termast.cmi 
-parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/environ.cmx \
-    kernel/generic.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    lib/pp.cmx kernel/term.cmx lib/util.cmx parsing/termast.cmi 
+parsing/termast.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
+    kernel/generic.cmi library/global.cmi library/goptions.cmi \
+    library/impargs.cmi kernel/inductive.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi parsing/termast.cmi 
+parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
+    kernel/generic.cmx library/global.cmx library/goptions.cmx \
+    library/impargs.cmx kernel/inductive.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx parsing/termast.cmi 
 pretyping/classops.cmo: kernel/environ.cmi kernel/generic.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi lib/pp.cmi \
     kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/classops.cmi 
diff --git a/lib/util.ml b/lib/util.ml
index ed56f06d7..77d26ecf4 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -62,6 +62,13 @@ let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
 let list_intersect l1 l2 = 
   List.filter (fun x -> List.mem x l2) l1
 
+let list_union l1 l2 = 
+  let rec urec = function
+    | [] -> l2
+    | a::l -> if List.mem a l2 then urec l else a::urec l
+  in 
+  urec l1
+
 let list_unionq l1 l2 = 
   let rec urec = function
     | [] -> l2
diff --git a/lib/util.mli b/lib/util.mli
index e0462b36c..30d7bdee7 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -36,6 +36,7 @@ val stringmap_dom : 'a Stringmap.t -> string list
 (*s Lists. *)
 
 val list_intersect : 'a list -> 'a list -> 'a list
+val list_union : 'a list -> 'a list -> 'a list
 val list_unionq : 'a list -> 'a list -> 'a list
 val list_subtract : 'a list -> 'a list -> 'a list
 val list_subtractq : 'a list -> 'a list -> 'a list
@@ -49,7 +50,6 @@ val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
diff --git a/library/impargs.ml b/library/impargs.ml
index 61a2c8b1a..a8fe59cc8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -23,6 +23,11 @@ let auto_implicits ty =
   else
     No_impl
 
+let list_of_implicits = function 
+  | Impl_auto l -> l
+  | Impl_manual l -> l
+  | No_impl -> []
+
 (* Constants. *)
 
 let constants_table = ref Spmap.empty
@@ -63,6 +68,17 @@ let constructor_implicits ((sp,i),j) =
   let imps = Spmap.find sp !inductives_table in
   (snd imps.(i)).(pred j)
 
+let mconstr_implicits mc = 
+  let (sp, i, j, _) = destMutConstruct mc in
+  list_of_implicits (constructor_implicits ((sp,i),j))
+
+let mind_implicits m =
+  let (sp,i,_) = destMutInd m in
+  list_of_implicits (inductive_implicits (sp,i))
+
+let implicits_of_var kind id =
+  failwith "TODO: implicits of vars"
+
 (* Registration as global tables and roolback. *)
 
 type frozen = implicits Spmap.t
@@ -85,3 +101,4 @@ let _ =
 let rollback f x =
   let fs = freeze () in
   try f x with e -> begin unfreeze fs; raise e end
+
diff --git a/library/impargs.mli b/library/impargs.mli
index 84ea98da3..51ada5845 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Names
+open Term
 (*i*)
 
 (* Implicit arguments. Here we store the implicit arguments. Notice that we 
@@ -15,6 +16,8 @@ type implicits =
 
 val implicit_args : bool ref
 
+val list_of_implicits : implicits -> int list
+
 val declare_constant_implicits : section_path -> unit
 val declare_constant_manual_implicits : section_path -> int list -> unit
 val constant_implicits : section_path -> implicits
@@ -23,4 +26,7 @@ val declare_inductive_implicits : section_path -> unit
 val inductive_implicits : section_path * int -> implicits
 val constructor_implicits : (section_path * int) * int -> implicits
 
+val mconstr_implicits : constr -> int list
+val mind_implicits : constr -> int list
+val implicits_of_var : Names.path_kind -> identifier -> int list
 
diff --git a/parsing/ast.ml b/parsing/ast.ml
index cb32a8b24..7b15a0f41 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -41,6 +41,10 @@ let rec set_loc loc = function
   | Path(_,sl,s) -> Path(loc,sl,s)
   | Dynamic(_,d) -> Dynamic(loc,d)
 
+let path_section loc sp =
+  let (sl,bn,pk) = repr_path sp in
+  Coqast.Path(loc,List.rev(string_of_id bn :: sl), string_of_kind pk)
+
 (* raising located exceptions *)
 let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 67ab4b94a..2663837f3 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -3,6 +3,7 @@
 
 (*i*)
 open Pp
+open Names
 open Pcoq
 (*i*)
 
@@ -28,6 +29,8 @@ val dynamic : Dyn.t -> Coqast.t
 
 val set_loc : Coqast.loc -> Coqast.t -> Coqast.t
 
+val path_section : Coqast.loc -> section_path -> Coqast.t
+
 (* ast destructors *)
 val num_of_ast : Coqast.t -> int
 val id_of_ast : Coqast.t -> string
diff --git a/parsing/termast.ml b/parsing/termast.ml
index edc31f294..040cd82ce 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -3,10 +3,14 @@
 
 open Pp
 open Util
+open Univ
 open Names
 open Generic
 open Term
-open Environ
+open Inductive
+open Sign
+open Declare
+open Impargs
 open Coqast
 open Ast
 
@@ -58,20 +62,22 @@ module StrongRenamingStrategy = struct
   let occur_id env id0 c =
     let rec occur n = function
       | VAR id             -> id=id0
-      | DOPN (Const sp,cl) -> (basename sp = id0) or (exists_vect (occur n) cl)
-      | DOPN (Abst sp,cl)  -> (basename sp = id0) or (exists_vect (occur n) cl)
+      | 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 (exists_vect (occur n) cl)
+	  (basename (mind_path t) = id0) or (array_exists (occur n) cl)
       | DOPN (MutConstruct _, cl) as t -> 
-	  (basename (mind_path t) = id0) or (exists_vect (occur n) cl)
-      | DOPN(_,cl)         -> exists_vect (occur n) cl
+	  (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)         -> exists_vect (occur (n+1)) v
+      | DLAMV(_,v)         -> array_exists (occur (n+1)) v
       | Rel p              ->
-	  p>n &
+	  p > n &
 	  (try (fst (lookup_rel (p-n) env) = Name id0)
 	   with Not_found -> false) (* Unbound indice : may happen in debug *)
       | DOP0 _             -> false
@@ -98,24 +104,24 @@ module StrongRenamingStrategy = struct
   let global_vars_and_consts t =
     let rec collect acc = function
       | VAR id             -> id::acc
-      | DOPN (Const sp,cl) -> (basename sp)::(it_vect collect acc cl)
-      | DOPN (Abst sp,cl)  -> (basename sp)::(it_vect collect acc cl)
+      | 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       -> 
-	  (basename (mind_path t))::(it_vect collect acc cl)
+	  (basename (mind_path t))::(Array.fold_left collect acc cl)
       | DOPN (MutConstruct _, cl) as t -> 
-	  (basename (mind_path t))::(it_vect collect acc cl)
-      | DOPN(_,cl)         -> it_vect collect acc cl
+	  (basename (mind_path t))::(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)         -> it_vect collect acc v
+      | DLAMV(_,v)         -> Array.fold_left collect acc v
       | _                  -> acc
     in 
-    uniquize (collect [] t)
+    list_uniquize (collect [] t)
 	 
   let used_of = global_vars_and_consts
-  let ids_of_env = Names.ids_of_env
+  let ids_of_env = Sign.ids_of_env
 end
 
 
@@ -134,8 +140,8 @@ let indsp_of_id id  =
 	  [< 'sTR ((string_of_id id)^" is not an inductive type") >]
 
 let mind_specif_of_mind_light (sp,tyi) =
-  let (_,mib) = mind_of_path sp in
-  (mib,Constrtypes.mind_nth_type_packet mib tyi)
+  let mib = Global.lookup_mind sp in
+  (mib,mind_nth_type_packet mib tyi)
 
 let rec remove_indtypes = function
   | (1, DLAMV(_,cl)) -> cl
@@ -155,13 +161,13 @@ let rec get_params = function
   | _                      -> []
 
 let lc_of_lmis (mib,mip) =
-  let lc = remove_indtypes (mib.mINDNTYPES,mip.mINDLC) in
-  Array.map (remove_params mib.mINDNPARAMS) lc
+  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.mINDTYPENAME) k
+  make_path pa (mip.mind_typename) k
 
 
 (* Parameterization of the translation from constr to ast      *)
@@ -190,7 +196,7 @@ module PrintingCasesMake =
       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 = Options.SecondaryTable ("Printing",Test.field)
+    let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
     let member_message = Test.member_message
     let synchronous = true
@@ -227,12 +233,12 @@ module PrintingCasesLet =
 	  ^ " are not printed using a `let' form"
   end)
 
-module PrintingIf  = Options.MakeTable(PrintingCasesIf)
-module PrintingLet = Options.MakeTable(PrintingCasesLet)
+module PrintingIf  = Goptions.MakeTable(PrintingCasesIf)
+module PrintingLet = Goptions.MakeTable(PrintingCasesLet)
 
 (* Options for printing or not wildcard and synthetisable types *)
 
-open Options
+open Goptions
 
 let wildcard_value = ref true
 let force_wildcard () = !wildcard_value
@@ -240,7 +246,7 @@ let force_wildcard () = !wildcard_value
 let _ = 			  
   declare_async_bool_option 
     { optasyncname  = "the forced wildcard option";
-      optasynckey   = Options.SecondaryTable ("Printing","Wildcard");
+      optasynckey   = SecondaryTable ("Printing","Wildcard");
       optasyncread  = force_wildcard;
       optasyncwrite = (fun v -> wildcard_value := v) }
 
@@ -250,7 +256,7 @@ let synthetize_type () = !synth_type_value
 let _ = 
   declare_async_bool_option 
     { optasyncname = "the synthesisablity";
-      optasynckey   = Options.SecondaryTable ("Printing","Synth");
+      optasynckey   = SecondaryTable ("Printing","Synth");
       optasyncread = synthetize_type;
       optasyncwrite = (fun v -> synth_type_value := v) }
 
@@ -291,7 +297,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
       match c with
         | DOPN(MutConstruct _,_) -> mconstr_implicits c
 	| DOPN(MutInd _,_) -> mind_implicits c
-	| DOPN(Const _,_) -> constant_implicits c
+	| DOPN(Const sp,_) -> list_of_implicits (constant_implicits sp)
 	| VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
 	| _ -> []
     in
@@ -326,7 +332,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
     let rec combine_rec = function
       | [] -> [],[]
       | NODE ((a,b),_)::l -> 
-	  let a',b' = combine_rec l in (union a a',union b b')
+	  let a',b' = combine_rec l in (list_union a a',list_union b b')
     in 
     NODE (combine_rec l,l)
 
@@ -384,13 +390,13 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 			bdrec avoid' (add_rel (Name id,()) env) c)
                | (None,avoid') -> slam(None,bdrec avoid' env (pop c)))
 	| DLAMV(na,cl) ->
-	    if not(exists_vect (dependent (Rel 1)) cl) then
-	      slam(None,ope("V$", map_vect_list 
+	    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$", map_vect_list 
+		   ope("V$", array_map_to_list 
 			 (bdrec (id::avoid) (add_rel (Name id,()) env)) cl))
 
         (* Well-formed constructions *)
@@ -404,14 +410,14 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
                (* TODO: Change this to subtract the current depth *)
 	       | IsMeta n -> ope("META",[num n])
 	       | IsVar id -> nvar (string_of_id id)
-	       | IsXtra (s,pl,cl) -> 
-		   ope("XTRA",((str s):: pl@(List.map (bdrec avoid env) cl)))
+	       | IsXtra s -> 
+		   ope("XTRA",[str s])
 	       | IsSort s ->
 		   (match s with
 		      | Prop c -> ope("PROP",[ide (str_of_contents c)])
 		      | Type u -> ope("TYPE",[path_section dummy_loc u.u_sp; 
 					      num u.u_num]))
-	       | IsImplicit -> ope("IMPLICIT",[])     
+	       (* TODO??? | IsImplicit -> ope("IMPLICIT",[]) *)
 	       | IsCast (c1,c2) ->
 		   if opcast = WithoutCast then 
 		     bdrec avoid env c1 
@@ -438,17 +444,19 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 
 	       | IsConst (sp,cl) ->
 		   ope("CONST",((path_section dummy_loc sp)::
-				(map_vect_list (bdrec avoid env) cl)))
+				(array_map_to_list (bdrec avoid env) cl)))
+	       | IsEvar (_,cl) ->
+		   ope("ISEVAR",(array_map_to_list (bdrec avoid env) cl))
 	       | IsAbst (sp,cl) ->
 		   ope("ABST",((path_section dummy_loc sp)::
-			       (map_vect_list (bdrec avoid env) cl)))
+			       (array_map_to_list (bdrec avoid env) cl)))
 	       | IsMutInd (sp,tyi,cl) ->
 		   ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
-				 (map_vect_list (bdrec avoid env) cl)))
+				 (array_map_to_list (bdrec avoid env) cl)))
 	       | IsMutConstruct (sp,tyi,n,cl) ->
 		   ope("MUTCONSTRUCT",
 		       ((path_section dummy_loc sp)::(num tyi)::(num n)::
-			(map_vect_list (bdrec avoid env) cl)))
+			(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
@@ -456,7 +464,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 		     | None -> 
 			 (* Pas d'annotation --> affichage avec vieux Case *)
 			 let pred = bdrec avoid env p in
-			 let bl' = map_vect_list (bdrec avoid env) bl in
+			 let bl' = array_map_to_list (bdrec avoid env) bl in
 			 ope("MUTCASE",pred::tomatch::bl')
 		     | Some indsp ->
 			 let (mib,mip as lmis) = 
@@ -464,7 +472,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 			 let lc = lc_of_lmis lmis in
 			 let lcparams = Array.map get_params lc in
 			 let k = 
-			   (nb_prod mip.mINDARITY.body) - mib.mINDNPARAMS in
+			   (nb_prod mip.mind_arity.body) - mib.mind_nparams in
 			 let pred = 
 			   if synth_type & computable p k & lcparams <> [||]
 			   then ope("XTRA", [str "SYNTH"])
@@ -475,11 +483,11 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 					    bdrec avoid env bl.(0); 
 					    bdrec avoid env bl.(1) ])
 			 else
-			   let idconstructs = mip.mINDCONSNAMES in
+			   let idconstructs = mip.mind_consnames in
 			   let asttomatch = 
 			     ope("XTRA",[str "TOMATCH"; tomatch]) in
 			   let eqnv = 
-			     map3_vect (bdize_eqn avoid env) idconstructs 
+			     array_map3 (bdize_eqn avoid env) idconstructs 
 			       lcparams bl in
 			   let eqnl = Array.to_list eqnv in
 			   let tag =
@@ -525,7 +533,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 		     | _ -> error "split_product" 
 		   in
 		   let listdecl = 
-		     map_i
+		     list_map_i
 		       (fun i fi ->
 			  let (lparams,ast_of_def) =
 			    split_lambda [] def_env def_avoid 
@@ -536,7 +544,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 			      [ nvar (string_of_id fi); 
 				ope ("BINDERS",List.rev lparams);
 				ast_of_typ; ast_of_def ]))
-		       0 lfi 
+		       0 lfi
 		   in 
 		   ope("FIX", (nvar (string_of_id f))::listdecl)
 
@@ -549,7 +557,7 @@ module MakeTermAst = functor (Strategy : RenamingStrategy) -> struct
 		   let def_avoid = lfi@avoid in
 		   let f = List.nth lfi n in
 		   let listdecl =
-		     map_i (fun i fi -> ope("CFDECL",
+		     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)]))