remplacement des deux constants prop/arity par une seule dummy + pretty-print des fix mutuels

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

8 files changed, 235 insertions, 205 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 20c558c504..fa2968c3fb 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -86,42 +86,43 @@ let decl_get_modules ld =
 				  List.iter (mltype_get_modules m) l) l) l
     | Dabbrev (_,_,t) -> mltype_get_modules m t 
     | Dglob (_,a) -> ast_get_modules m a
+    | Dfix(_,c) -> Array.iter (ast_get_modules m) c  
     | _ -> ()
   in 
   List.iter one_decl ld; 
   !m
 
-(*s Does [prop] or [arity] occur ? *)
+(*s Does [Tdummy] or [MLdummy] occur ? *)
 
-exception Print_prop
+exception Found
 
-let ast_print_prop a = 
+let ast_mem_dummy a = 
   let rec get_rec = function 
-    | MLprop | MLarity -> raise Print_prop
+    | MLdummy -> raise Found
     | a -> ast_iter get_rec a
   in get_rec a
 
-let mltype_print_prop t = 
+let type_mem_dummy t = 
   let rec get_rec = function 
-    | Tprop | Tarity -> raise Print_prop
+    | Tdummy -> raise Found
     | Tapp l -> List.iter get_rec l
     | Tarr (a,b) -> get_rec a; get_rec b 
     | _ -> () 
   in get_rec t
 
-let decl_print_prop ld = 
+let decl_mem_dummy ld = 
   let one_decl = function 
     | Dtype (l,_) -> 
 	List.iter (fun (_,_,l) -> 
-		     List.iter (fun (_,l) -> 
-				  List.iter mltype_print_prop l) l) l
-    | Dabbrev (_,_,t) -> mltype_print_prop t 
-    | Dglob (_,a) -> ast_print_prop a
+		     List.iter (fun (_,l) -> List.iter type_mem_dummy l) l) l
+    | Dabbrev (_,_,t) -> type_mem_dummy t 
+    | Dglob (_,a) -> ast_mem_dummy a
+    | Dfix(_,c) -> Array.iter ast_mem_dummy c
     | _ -> ()
   in 
   try 
     List.iter one_decl ld; false 
-  with Print_prop -> true
+  with Found -> true
 
 (*s Tables of global renamings *)
 
@@ -262,7 +263,7 @@ let extract_to_file f prm decls =
   if not prm.modular then 
     List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
       (List.filter decl_is_singleton prm.to_appear); 
-  pp_with ft (preamble prm used_modules (decl_print_prop decls));
+  pp_with ft (preamble prm used_modules (decl_mem_dummy decls));
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 78d89b6695..ef4b5c9e44 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -55,14 +55,16 @@ let check_decl m sm = function
   | Dtype ((_,r,_)::_, _) -> check_r m sm r 
   | Dtype ([],_) -> ()
   | Dcustom (r,_) ->  check_r m sm r
+  | Dfix(rv,_) -> Array.iter (check_r m sm) rv 
 
-(* [check_one_module m l] checks that no module names in [l] clashes with [m]. *)
+(* [check_one_module] checks that no module names in [l] clashes with [m]. *)
 
 let check_one_module m l = 
   let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in 
   List.iter (check_decl m sm) l
 
-(* [check_modules m] checks if there are conflicts within the set [m] of modules dirpath. *) 
+(* [check_modules] checks if there are conflicts within the set [m] 
+   of modules dirpath. *) 
 
 let check_modules m = 
   let map = ref Idmap.empty in 
@@ -138,7 +140,7 @@ and visit_type m eenv t =
     | Tglob r -> visit_reference m eenv r
     | Tapp l -> List.iter visit l
     | Tarr (t1,t2) -> visit t1; visit t2
-    | Tvar _ | Tprop | Tarity -> ()
+    | Tvar _ | Tdummy -> ()
   in
   visit t
     
@@ -155,7 +157,7 @@ and visit_ast m eenv a =
     | MLfix (_,_,l) -> Array.iter visit l
     | MLcast (a,t) -> visit a; visit_type m eenv t
     | MLmagic a -> visit a
-    | MLrel _ | MLprop | MLarity | MLexn _ -> ()
+    | MLrel _ | MLdummy | MLexn _ -> ()
   in
   visit a
 
@@ -169,6 +171,7 @@ and visit_decl m eenv = function
   | Dabbrev (_,_,t) -> visit_type m eenv t
   | Dglob (_,a) -> visit_ast m eenv a
   | Dcustom _ -> ()
+  | Dfix (_,c) -> Array.iter (visit_ast m eenv) c
 	
 (*s Recursive extracted environment for a list of reference: we just
     iterate [visit_reference] on the list, starting with an empty
@@ -204,6 +207,7 @@ let decl_in_r r0 = function
   | Dtype ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
   | Dtype ([],_) -> false
   | Dcustom (r,_) ->  r = r0 
+  | Dfix (rv,_) -> array_exists ((=) r0) rv
 
 let pp_decl d = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_decl d
@@ -309,6 +313,7 @@ let decl_in_m m = function
   | Dtype ((_,r,_)::_, _) -> is_long_module m r 
   | Dtype ([],_) -> false
   | Dcustom (r,_) ->  is_long_module m r
+  | Dfix (rv,_) -> is_long_module m rv.(0)
 
 let module_file_name m = match lang () with 
   | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 93444bf8bb..63280670a1 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -69,14 +69,16 @@ type signature = type_var list
    that extracts a CIC object into an ML type. It is either: 
    \begin{itemize}
    \item a real ML type, followed by its list of type variables (['a],\ldots)
+   \item a dummy type, denoting either: 
+   \begin{itemize} 
    \item a CIC arity, without counterpart in ML
    \item a non-informative type, which will receive special treatment
+   \end{itemize}
    \end{itemize} *)
 
 type type_extraction_result =
   | Tmltype of ml_type * identifier list
-  | Tarity
-  | Tprop
+  | Tdum
 
 (* The [indutive_extraction_result] is the dual of [type_extraction_result], 
    but for inductive types. *)
@@ -153,13 +155,16 @@ let is_axiom sp = (Global.lookup_constant sp).const_body = None
 
 type lamprod = Lam | Product
 
+let dummy_arrow = function 
+  | Tmltype (mld,vl) -> Tmltype (Tarr (Tdummy, mld), vl)
+  | Tdum -> Tdum
+
 (*s [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t]
    returns the list [[a;b;...;z]]. It is used when making the ML types
    of inductive definitions. We also suppress [prop] and [arity] parts. *)
 
 let rec list_of_ml_arrows = function
-  | Tarr (Miniml.Tarity, b) -> list_of_ml_arrows b
-  | Tarr (Miniml.Tprop, b) -> list_of_ml_arrows b
+  | Tarr (Tdummy, b) -> list_of_ml_arrows b
   | Tarr (a, b) -> a :: list_of_ml_arrows b
   | t -> []
 
@@ -233,9 +238,8 @@ let expansion_prop_eta s (ids,c) =
     | [] -> 
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
 	in ids, MLapp (ml_lift (i-1) c, a) 
-    | (_,Arity) :: l -> abs (prop_name :: ids) (MLarity :: rels) (succ i) l
-    | (Logic,_) :: l -> abs (prop_name :: ids) (MLprop :: rels) (succ i) l
-    | (Info,_) :: l -> abs (anonymous :: ids) (MLrel i :: rels) (succ i) l
+    | (Info,NotArity) :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
+    | _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
   in abs ids [] 1 s
 
 let kill_all_prop_lams_eta e s = 
@@ -247,7 +251,7 @@ let kill_all_prop_lams_eta e s =
 
 let kill_prop_lams_eta e s =
   let ids,e = kill_all_prop_lams_eta e s in 
-  if ids = [] then MLlam (prop_name, ml_lift 1 e)
+  if ids = [] then MLlam (dummy_name, ml_lift 1 e)
   else named_lams ids e
 
 (*s Auxiliary function for [abstract_constant] and [abstract_constructor]. *)
@@ -255,7 +259,7 @@ let kill_prop_lams_eta e s =
 let prop_abstract f  = 
   let rec abs rels i = function 
     | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels)
-    | ((_,Arity)|(Logic,_)) :: l -> MLlam (prop_name, abs rels (succ i) l)
+    | ((_,Arity)|(Logic,_)) :: l -> MLlam (dummy_name, abs rels (succ i) l)
     | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l)
   in abs [] 1  
 
@@ -264,7 +268,7 @@ let prop_abstract f  =
 let abstract_constant sp s = 
   let f a = 
     if List.mem default s then MLapp (MLglob (ConstRef sp), a)
-    else MLapp (MLglob (ConstRef sp), [MLprop]) (* or MLarity, I don't mind *)
+    else MLapp (MLglob (ConstRef sp), [MLdummy])
   in prop_abstract f s
 
 (*S Error messages. *)
@@ -286,9 +290,10 @@ let section_message () =
 (* Relation with [v_of_t]: it is less precise, since we do not 
    delta-reduce in [extract_type] in general.
    \begin{itemize}
-   \item If [v_of_t env t = NotArity,_], 
+   \item If [v_of_t env t = _,NotArity], 
    then [extract_type env t] is a [Tmltype].
-   \item If [extract_type env t = Tarity], then [v_of_t env t = Arity,_]
+   \item If [extract_type env t = Tdum], then [v_of_t env t = _,Arity]
+   or [Logic,NotArity].
    \end{itemize} *)
 
 (* Generation of type variable list (['a] in caml).
@@ -309,17 +314,15 @@ and extract_type_rec env c vl args =
   (* [t] is an arity of sort [Prop], or *)
   (* [c] has a non-informative head symbol *)
   match get_arity env t with 
-    | None -> 
-	assert false (* Cf. precondition. *)
-    | Some InProp ->
-	Tprop 
+    | None -> assert false (* Cf. precondition. *)
+    | Some InProp -> Tdum 
     | Some _ -> extract_type_rec_info env c vl args
 	  
 and extract_type_rec_info env c vl args = 
   match (kind_of_term (betaiotazeta env none c)) with
     | Sort _ ->
 	assert (args = []); (* A sort can't be applied. *)
-	Tarity 
+	Tdum 
     | Prod (n,t,d) ->
 	assert (args = []); (* A product can't be applied. *)
 	extract_prod_lam env (n,t,d) vl Product
@@ -338,14 +341,13 @@ and extract_type_rec_info env c vl args =
     | Const sp when args = [] && is_ml_extraction (ConstRef sp) ->
 	Tmltype (Tglob (ConstRef sp), vl)
     | Const sp when is_axiom sp -> 
-	let id = next_ident_away (basename sp) (prop_name::vl) in 
+	let id = next_ident_away (basename sp) (dummy_name::vl) in 
 	Tmltype (Tvar id,  id :: vl)
     | Const sp ->
 	let t = constant_type env sp in 
 	if is_arity env none t then
 	  (match extract_constant sp with 
-	     | Emltype (Miniml.Tarity,_,_) -> Tarity
-	     | Emltype (Miniml.Tprop,_,_) -> Tprop
+	     | Emltype (Tdummy,_,_) -> Tdum
 	     | Emltype (_, sc, vlc) ->  
 		 extract_type_app env (ConstRef sp,sc,vlc) vl args 
 	     | Emlterm _ -> assert false) 
@@ -360,7 +362,7 @@ and extract_type_rec_info env c vl args =
 	       extract_type_app env (IndRef spi,si,vli) vl args 
 	   |Iprop -> assert false (* Cf. initial tests *))
     | Case _ | Fix _ | CoFix _ ->
-	let id = next_ident_away flex_name (prop_name::vl) in
+	let id = next_ident_away flex_name (dummy_name::vl) in
 	Tmltype (Tvar id,  id :: vl)
 	  (* Type without counterpart in ML: we generate a 
 	     new flexible type variable. *) 
@@ -376,25 +378,29 @@ and extract_prod_lam env (n,t,d) vl flag =
   let tag = v_of_t env t in
   let env' = push_rel_assum (n,t) env in
   match tag,flag with
-    | (Info, Arity), _ -> 
+    | (Info, Arity), Lam -> 
+	(* We rename before the [push_rel], to be sure that the corresponding*)
+	(* [lookup_rel] will be correct. *)
+	let id' = next_ident_away (id_of_name n) vl in 
+	let env' = push_rel_assum (Name id', t) env in
+	extract_type_rec_info env' d (id'::vl) []
+    | _, Lam ->
+	extract_type_rec_info  env' d vl []
+    | (Info, Arity), Product -> 
 	(* We rename before the [push_rel], to be sure that the corresponding*)
 	(* [lookup_rel] will be correct. *)
 	let id' = next_ident_away (id_of_name n) vl in 
 	let env' = push_rel_assum (Name id', t) env in
-	extract_type_rec_info env' d (id'::vl) [] (* TODO !!!!!!!!!! *)
-    | (Logic, Arity), _ | _, Lam ->
-      extract_type_rec_info  env' d vl [] (* TODO !!!!!!!!!!!! *)
-    | (Logic, NotArity), Product ->
-      (match extract_type_rec_info env' d vl [] with 
-         | Tmltype (mld, vl') -> Tmltype (Tarr (Miniml.Tprop, mld), vl')
-         | et -> et)
+	dummy_arrow (extract_type_rec_info env' d (id'::vl) [])
+    | (Logic,_), Product -> 
+	dummy_arrow (extract_type_rec_info env' d vl [])
     | (Info, NotArity), Product ->
 	(* It is important to treat [d] first and [t] in second. *)
 	(* This ensures that the end of [vl] correspond to external binders. *)
 	(match extract_type_rec_info env' d vl [] with 
 	   | Tmltype (mld, vl') -> 
 	       (match extract_type_rec_info env t vl' [] with
-		  | Tprop | Tarity -> assert false 
+		  | Tdum -> assert false 
 			(* Cf. relation between [extract_type] and [v_of_t] *)
 		  | Tmltype (mlt,vl'') -> Tmltype (Tarr(mlt,mld), vl''))
 	   | et -> et)
@@ -422,9 +428,8 @@ and extract_type_app env (r,sc,vlc) vl args =
 	 | _, NotArity -> acc
 	 | Logic, Arity -> acc
 	 | Info, Arity -> match extract_type_rec_info env a vl [] with
-	     | Tarity -> (Miniml.Tarity :: args, vl) 
+	     | Tdum -> (Tdummy :: args, vl) 
   	           (* we pass a dummy type [arity] as argument *)
-	     | Tprop -> (Miniml.Tprop :: args, vl)
 	     | Tmltype (mla,vl') -> (mla :: args, vl'))
       (List.combine sign_args args) 
       ([],vl)
@@ -435,7 +440,7 @@ and extract_type_app env (r,sc,vlc) vl args =
   assert (nvlargs >= 0);
   let vl'' = 
     List.fold_right 
-      (fun id l -> (next_ident_away id (prop_name::l)) :: l) 
+      (fun id l -> (next_ident_away id (dummy_name::l)) :: l) 
       (list_firstn nvlargs vlc) vl'
   in
   (* We complete the list of arguments of [c] by variables *)
@@ -472,8 +477,7 @@ and signature_rec env c args =
         let t = constant_type env sp in
         if is_arity env none t then
           (match extract_constant sp with
-             | Emltype (Miniml.Tarity,_,_) -> []
-             | Emltype (Miniml.Tprop,_,_) -> []
+             | Emltype (Tdummy,_,_) -> []
              | Emltype (_,sc,_) ->
                  let d = List.length sc - List.length args in
                  if d <= 0 then [] else list_lastn d sc
@@ -517,18 +521,16 @@ and extract_term_wt env c t =
 	 let id = id_of_name n in 
 	 (* If [d] was of type an arity, [c] too would be so *)
 	 let d' = extract_term (push_rel_assum (Name id,t) env) d in
-	 if (v_of_t env t)=default then MLlam (id, d')
-	 else MLlam(prop_name, d')
+	 if (v_of_t env t) = default then MLlam (id, d')
+	 else MLlam (dummy_name, d')
      | LetIn (n, c1, t1, c2) ->
 	 let id = id_of_name n in 
 	 (* If [c2] was of type an arity, [c] too would be so *)
 	 let c2' = extract_term (push_rel (Name id,Some c1,t1) env) c2 in
-	 (match v_of_t env t1 with
-	    | _,Arity -> MLletin (prop_name,MLarity,c2')
-	    | Logic,NotArity -> MLletin (prop_name, MLprop, c2')
-	    | Info, NotArity -> 
-		let c1' = extract_term_wt env c1 t1 in 
-		MLletin (id,c1',c2'))
+	 if (v_of_t env t1) = default then 
+	   let c1' = extract_term_wt env c1 t1 in 
+	   MLletin (id,c1',c2')
+	 else MLletin (dummy_name, MLdummy, c2')
      | Rel n ->
 	 MLrel n
      | Const sp ->
@@ -567,7 +569,7 @@ and extract_term_wt env c t =
 and abstract_constructor cp (s,params_nb) =
   let f a = if is_singleton_constructor cp then List.hd a
   else MLcons (ConstructRef cp, a)
-  in prop_lams (ml_lift params_nb (prop_abstract f s)) params_nb
+  in dummy_lams (ml_lift params_nb (prop_abstract f s)) params_nb
 
 (*s Extraction of a case. *)
 
@@ -640,8 +642,8 @@ and extract_app env f args =
   let mlargs = 
     List.fold_right 
       (fun (v,a) args -> match v with
-	 | (_,Arity) -> MLarity :: args
-	 | (Logic,NotArity) -> MLprop :: args
+	 | (_,Arity) -> MLdummy :: args
+	 | (Logic,NotArity) -> MLdummy :: args
 	 | (Info,NotArity) -> 
 	     (* We can't trust tag [default], so we use [extract_constr]. *)
 	     (extract_constr_to_term env a) :: args)
@@ -680,8 +682,8 @@ and extract_constr_to_term env c =
 
 and extract_constr_to_term_wt env c t = 
   match v_of_t env t with
-    | (_, Arity) -> MLarity 
-    | (Logic, NotArity) -> MLprop
+    | (_, Arity) -> MLdummy 
+    | (Logic, NotArity) -> MLdummy
     | (Info, NotArity) -> extract_term_wt env c t
 
 (*S Extraction of a constr. *)
@@ -693,12 +695,11 @@ and extract_constr env c =
 
 and extract_constr_wt env c t =
   match v_of_t env t with
-    | (Logic, Arity) -> Emltype (Miniml.Tarity, [], [])
-    | (Logic, NotArity) -> Emlterm MLprop
+    | (Logic, Arity) -> Emltype (Tdummy, [], [])
+    | (Logic, NotArity) -> Emlterm MLdummy
     | (Info, Arity) -> 
 	(match extract_type env c with
-	   | Tprop -> Emltype (Miniml.Tprop, [], [])
-	   | Tarity -> Emltype (Miniml.Tarity, [], [])
+	   | Tdum -> Emltype (Tdummy, [], [])
 	   | Tmltype (t, vl) -> Emltype (t, (signature env c), vl))
     | (Info, NotArity) -> 
 	Emlterm (extract_term_wt env c t)
@@ -715,12 +716,11 @@ and extract_constant sp =
       | None ->
           (match v_of_t env typ with
              | (Info,_) -> axiom_message sp (* We really need some code here *)
-             | (Logic,NotArity) -> Emlterm MLprop (* Axiom? I don't mind! *)
-             | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[]))  (* Idem *)
+             | (Logic,NotArity) -> Emlterm MLdummy (* Axiom? I don't mind! *)
+             | (Logic,Arity) -> Emltype (Tdummy,[],[]))  (* Idem *)
       | Some body ->
 	  let e = match extract_constr_wt env body typ with 
-	    | Emlterm MLprop as e -> e
-	    | Emlterm MLarity as e -> e
+	    | Emlterm MLdummy as e -> e
 	    | Emlterm a -> 
 		Emlterm (kill_prop_lams_eta a (signature_of_sp sp typ))
 	    | e -> e 
@@ -801,7 +801,7 @@ and extract_mib sp =
 		  let t = type_of_constructor env (ip,j) in
 		  let t = snd (decompose_prod_n params_nb t) in
 		  match extract_type_rec_info params_env t vl [] with
-		    | Tarity | Tprop -> assert false
+		    | Tdum -> assert false
 		    | Tmltype (mlt, v) -> 
 			let l = list_of_ml_arrows mlt
 			and s = signature params_env t in 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 201458bb74..7549f8f4d9 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -28,10 +28,10 @@ let keywords =
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_";
-    "as"; "qualified"; "hiding" ; "prop" ; "arity" ]
+    "as"; "qualified"; "hiding" ; "dummy" ; "Dummy" ]
   Idset.empty
 
-let preamble prm used_modules used_prop =
+let preamble prm used_modules used_dummy =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
@@ -40,15 +40,12 @@ let preamble prm used_modules used_prop =
        s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl())
     used_modules (mt ())
   ++ 
-  (if used_prop then 
+  (if used_dummy then 
      str "import qualified Unit" ++ fnl () ++ fnl () ++
-     str "type Prop = Unit.Unit" ++ fnl () ++
-     str "prop = Unit.unit" ++ fnl () ++ fnl () ++
-     str "data Arity = Unit.Unit" ++ fnl () ++
-     str "arity = Unit.unit" ++ fnl () ++ fnl () 
+     str "type Dummy = Unit.Unit" ++ fnl () ++
+     str "dummy = Unit.unit" ++ fnl () ++ fnl ()
    else fnl ())
 
-
 let pp_abst = function
   | [] -> (mt ())
   | l  -> (str "\\" ++
@@ -87,8 +84,7 @@ let rec pp_type par ren t =
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
     | Tglob r -> pp_type_global r
-    | Tprop -> str "Prop"
-    | Tarity -> str "Arity"
+    | Tdummy -> str "Dummy"
   in 
   hov 0 (pp_rec par t)
 
@@ -159,10 +155,8 @@ let rec pp_expr par env args =
 	(* An [MLexn] may be applied, but I don't really care. *)
 	(open_par par ++ str "Prelude.error" ++ spc () ++ 
 	 qs s ++ close_par par)
-    | MLprop ->
-	str "prop" (* An [MLprop] may be applied, but I don't really care. *)
-    | MLarity ->
-	str "arity" (* Idem for [MLarity].*)
+    | MLdummy ->
+	str "dummy" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
 	let tvars = get_tvars t in 
 	let _,ren = rename_tvars keywords tvars in 
@@ -257,28 +251,16 @@ let pp_decl = function
 	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
 	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
 	       pp_type false ren t ++ fnl ())
-  | Dglob (r, MLfix (_,[|_|],[|def|])) ->
-      let id = rename_global r in
-      let env' = [id], P.globals() in
-      (pp_function  env' (pr_id id) def ++ fnl ())
-(*  | Dglob (r, MLfix (i,ids,defs)) ->
-      let env = empty_env () in
-      let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      (prlist_with_sep (fun () -> (fnl ()))
-	   (fun (fi,ti) -> pp_function env' (pr_id fi) ti)
-	   (List.combine (List.rev ids') (Array.to_list defs)) ++
-	 fnl () ++
-	 let id = rename_global r in
-	 let idi = List.nth (List.rev ids') i in
-	 if id <> idi then
-	   (fnl () ++ pr_id id ++ str " = " ++ pr_id idi ++ fnl ())
-	 else
-	   (mt ())) *)
+  | Dfix (rv, defs) ->
+      let ids = List.map rename_global (Array.to_list rv) in 
+      let env = List.rev ids, P.globals() in
+      (prlist_with_sep (fun () -> fnl () ++ fnl ()) 
+	   (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	   (List.combine ids (Array.to_list defs)) ++ fnl ())
   | Dglob (r, a) ->
       hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
   | Dcustom (r,s) -> 
-      hov 0  (pp_global r ++ str " =" ++ 
-		spc () ++ str s ++ fnl ())
+      hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
 
 let pp_type = pp_type false Idmap.empty
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 60d5baf402..8637bc8b55 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -22,8 +22,7 @@ type ml_type =
   | Tapp  of ml_type list
   | Tarr  of ml_type * ml_type
   | Tglob of global_reference
-  | Tprop
-  | Tarity
+  | Tdummy
       
 (*s ML inductive types. *)
 
@@ -42,8 +41,7 @@ type ml_ast =
   | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
   | MLfix   of int * identifier array * ml_ast array
   | MLexn   of string
-  | MLprop
-  | MLarity
+  | MLdummy
   | MLcast  of ml_ast * ml_type
   | MLmagic of ml_ast
 
@@ -54,6 +52,7 @@ type ml_decl =
   | Dabbrev of global_reference * identifier list * ml_type
   | Dglob   of global_reference * ml_ast
   | Dcustom of global_reference * string
+  | Dfix    of global_reference array * ml_ast array
 
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 0af628b7ac..f8fc287c54 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -29,12 +29,12 @@ exception Impossible
 (*S Names operations. *)
 
 let anonymous = id_of_string "x"
-let prop_name = id_of_string "_"
+let dummy_name = id_of_string "_"
 let flex_name = id_of_string "flex"
 
 let id_of_name = function
   | Anonymous -> anonymous
-  | Name id when id = prop_name -> anonymous
+  | Name id when id = dummy_name -> anonymous
   | Name id -> id 
 
 (*S Operations upon ML types. *)
@@ -92,7 +92,7 @@ let ast_iter_rel f =
     | MLcons (_,l) ->  List.iter (iter n) l
     | MLcast (a,_) -> iter n a
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLprop | MLarity -> ()
+    | MLglob _ | MLexn _ | MLdummy -> ()
   in iter 0 
 
 (*s Map over asts. *)
@@ -108,7 +108,7 @@ let ast_map f = function
   | MLcons (c,l) -> MLcons (c, List.map f l)
   | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -124,7 +124,7 @@ let ast_map_lift f n = function
   | MLcons (c,l) -> MLcons (c, List.map (f n) l)
   | MLcast (a,t) -> MLcast (f n a, t)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a	
 
 (*s Iter over asts. *) 
 
@@ -139,7 +139,7 @@ let ast_iter f = function
   | MLcons (c,l) -> List.iter f l
   | MLcast (a,t) -> f a
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -259,19 +259,19 @@ let rec nb_lams = function
 
 let rec named_lams ids a = match ids with 
   | [] -> a 
-  | id :: ids -> named_lams ids (MLlam(id,a))
+  | id :: ids -> named_lams ids (MLlam (id,a))
 
 (*s The same in anonymous version. *)
 
 let rec anonym_lams a = function 
   | 0 -> a 
-  | n -> anonym_lams (MLlam(anonymous,a)) (pred n)
+  | n -> anonym_lams (MLlam (anonymous,a)) (pred n)
 
-(*s Idem for [prop_name]. *)
+(*s Idem for [dummy_name]. *)
 
-let rec prop_lams a = function 
+let rec dummy_lams a = function 
   | 0 -> a 
-  | n -> anonym_lams (MLlam(prop_name,a)) (pred n)
+  | n -> anonym_lams (MLlam (dummy_name,a)) (pred n)
 
 (*S Operations concerning eta. *)
 
@@ -286,7 +286,7 @@ let rec test_eta_args_lift k n = function
   | [] -> n=0
   | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
 
-(*s Computes a eta-reduction. *)
+(*s Computes an eta-reduction. *)
 
 let eta_red e = 
   let ids,t = collect_lams e in 
@@ -295,10 +295,11 @@ let eta_red e =
   else match t with 
     | MLapp (f,a) -> 
 	let m = (List.length a) - n in 
-	if m < 0 then e else
-	  let a',a'' = list_chop m a in 
-	  let f = if m = 0 then f else MLapp (f,a') in 
-	  if test_eta_args_lift 0 n a'' && not (occurs_itvl 1 n f)
+	if m < 0 then e 
+	else
+	  let a1,a2 = list_chop m a in 
+	  let f = if m = 0 then f else MLapp (f,a1) in 
+	  if test_eta_args_lift 0 n a2 && not (occurs_itvl 1 n f)
 	  then ml_lift (-n) f
 	  else e 
     | _ -> e
@@ -322,12 +323,18 @@ let check_and_generalize (r0,l,c) =
     | a -> ast_map_lift genrec n a
   in genrec 0 c  
 
+(*s [check_generalizable_case] checks if all branches can be seen as the 
+  same function [f] applied to the term matched. It is a generalized version 
+  of the identity case optimization. *)
+
 let check_generalizable_case br = 
   let f = check_and_generalize br.(0) in 
   for i = 1 to Array.length br - 1 do 
     if check_and_generalize br.(i) <> f then raise Impossible 
   done; f
 
+(*s Do all branches correspond to the same thing? *)
+
 let check_constant_case br = 
   if br = [||] then raise Impossible; 
   let (r,l,t) = br.(0) in
@@ -341,21 +348,28 @@ let check_constant_case br =
     then raise Impossible
   done; cst
 
-(* TODO: il faudrait verifier si dans chaque branche on a [_] et non pas 
-   seulement dans la premiere (Coercion Prop < Type). *) 
+(*s If all branches are functions, try to permut the case and the functions. *)
+
+let rec merge_ids ids ids' = match ids,ids' with 
+  | [],[] -> [] 
+  | i::ids, i'::ids' -> 
+      (if i = dummy_name then i' else i) :: (merge_ids ids ids')
+  | _ -> assert false 
 
 let rec permut_case_fun br acc = 
   let br = Array.copy br in 
   let (_,_,t0) = br.(0) in 
   let nb = ref (nb_lams t0) in 
   Array.iter (fun (_,_,t) -> let n = nb_lams t in if n < !nb then nb:=n) br;
-  let ids,_ = collect_n_lams !nb t0 in 
+  let ids = ref (fst (collect_n_lams !nb t0)) in  
+  Array.iter 
+    (fun (_,_,t) -> ids := merge_ids !ids (fst (collect_n_lams !nb t))) br; 
   for i = 0 to Array.length br - 1 do 
     let (r,l,t) = br.(i) in 
     let t = permut_rels !nb (List.length l) (remove_n_lams !nb t) 
     in br.(i) <- (r,l,t)
   done; 
-  (ids,br)
+  (!ids,br)
   
 (*S Generalized iota-reduction. *)
 
@@ -387,7 +401,7 @@ let iota_gen br =
   in iota 0 
 
 let is_atomic = function 
-  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity -> true
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
   | _ -> false
 
 (*S The main simplification function. *)
@@ -403,7 +417,7 @@ let rec simpl o = function
       let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in 
       simpl_case o br (simpl o e) 
   | MLletin(id,c,e) when 
-      (id = prop_name) || (is_atomic c) || (nb_occur e <= 1) -> 
+      (id = dummy_name) || (is_atomic c) || (nb_occur e <= 1) -> 
 	simpl o (ml_subst c e)
   | MLletin(_,c,e) when (is_atomic (eta_red c)) -> 
       simpl o (ml_subst (eta_red c) e)
@@ -416,7 +430,7 @@ let rec simpl o = function
 
 and simpl_app o a = function  
   | MLapp (f',a') -> simpl_app o (a'@a) f'
-  | MLlam (id,t) when id = prop_name -> 
+  | MLlam (id,t) when id = dummy_name -> 
       simpl o (MLapp (ml_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
       (match nb_occur t with
@@ -437,7 +451,7 @@ and simpl_app o a = function
 	     let a' = List.map (ml_lift k) a in
       	     (n, l, simpl o (MLapp (t,a')))) br 
       in simpl o (MLcase (e,br')) 
-  | (MLarity | MLprop | MLexn _) as e -> e 
+  | (MLdummy | MLexn _) as e -> e 
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
@@ -495,25 +509,25 @@ let kill_some_lams bl (ids,c) =
     select_via_bl bl ids, gen_subst v (n'-n) c
   end
 
-(*s [kill_prop_lams] uses the last function to kill the lambdas corresponding 
-  to a [prop_name]. It can raise [Impossible] if there is nothing to do, or 
+(*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding 
+  to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or 
   if there is no lambda left at all. *)
 
-let kill_prop_lams c = 
+let kill_dummy_lams c = 
   let ids,c = collect_lams c in 
-  let bl = List.map ((<>) prop_name) ids in 
+  let bl = List.map ((<>) dummy_name) ids in 
   if (List.mem true bl) && (List.mem false bl) then 
     let ids',c = kill_some_lams bl (ids,c) in 
     ids, named_lams ids' c
   else raise Impossible
       
-(*s [kill_prop_args ids t0 t] looks for occurences of [t0] in [t] and 
-  purge the args of [t0] corresponding to a [prop_name]. 
+(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and 
+  purge the args of [t0] corresponding to a [dummy_name]. 
   It makes eta-expansion if needed. *) 
 
-let kill_prop_args ids t0 t =
+let kill_dummy_args ids t0 t =
   let m = List.length ids in 
-  let bl = List.rev_map ((<>) prop_name) ids in
+  let bl = List.rev_map ((<>) dummy_name) ids in
   let rec killrec n = function 
     | MLapp(e, a) when e = ml_lift n t0 -> 
 	let k = max 0 (m - (List.length a)) in 
@@ -527,56 +541,54 @@ let kill_prop_args ids t0 t =
     | e -> ast_map_lift killrec n e 
   in killrec 0 t 
 
-(*s The main function for local [prop] elimination. *)
+(*s The main function for local [dummy] elimination. *)
 
-let rec kill_prop = function 
+let rec kill_dummy = function 
   | MLfix(i,fi,c) -> 
       (try 
-	 let ids,c = kill_prop_fix i fi c in 
-	 ml_subst (MLfix (i,fi,c)) (kill_prop_args ids (MLrel 1) (MLrel 1))
-       with Impossible -> MLfix (i,fi,Array.map kill_prop c))
+	 let ids,c = kill_dummy_fix i fi c in 
+	 ml_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
+       with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
   | MLapp (MLfix (i,fi,c),a) -> 
       (try 
-	 let ids,c = kill_prop_fix i fi c in 
-	 let a = List.map (fun t -> ml_lift 1 (kill_prop t)) a in 
-	 let e = kill_prop_args ids (MLrel 1) (MLapp (MLrel 1,a)) in
+	 let ids,c = kill_dummy_fix i fi c in 
+	 let a = List.map (fun t -> ml_lift 1 (kill_dummy t)) a in 
+	 let e = kill_dummy_args ids (MLrel 1) (MLapp (MLrel 1,a)) in
 	 ml_subst (MLfix (i,fi,c)) e  
        with Impossible -> 
-	 MLapp(MLfix(i,fi,Array.map kill_prop c),List.map kill_prop a))
+	 MLapp(MLfix(i,fi,Array.map kill_dummy c),List.map kill_dummy a))
   | MLletin(id, MLfix (i,fi,c),e) -> 
       (try 
-	 let ids,c = kill_prop_fix i fi c in
-	 let e = kill_prop (kill_prop_args ids (MLrel 1) e) in 
+	 let ids,c = kill_dummy_fix i fi c in
+	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in 
 	 MLletin(id, MLfix(i,fi,c),e)
       with Impossible -> 
-	MLletin(id, MLfix(i,fi,Array.map kill_prop c),kill_prop e))
+	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
   | MLletin(id,c,e) -> 
       (try 
-	 let ids,c = kill_prop_lams c in 
-	 let e = kill_prop_args ids (MLrel 1) e in 
-	 MLletin (id, kill_prop c,kill_prop e) 
-       with Impossible -> MLletin(id,kill_prop c,kill_prop e))
-  | a -> ast_map kill_prop a
+	 let ids,c = kill_dummy_lams c in 
+	 let e = kill_dummy_args ids (MLrel 1) e in 
+	 MLletin (id, kill_dummy c,kill_dummy e) 
+       with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
+  | a -> ast_map kill_dummy a
 
-and kill_prop_fix i fi c = 
+and kill_dummy_fix i fi c = 
   let n = Array.length fi in 
-  let ids,ci = kill_prop_lams c.(i) in 
+  let ids,ci = kill_dummy_lams c.(i) in 
   let c = Array.copy c in c.(i) <- ci; 
   for j = 0 to (n-1) do 
-    c.(j) <- kill_prop (kill_prop_args ids (MLrel (n-i)) c.(j)) 
+    c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j)) 
   done;
   ids,c
 
 (*s Putting things together. *)
 
 let normalize a = 
-  if (optim()) then kill_prop (simpl true a) else simpl false a
+  if (optim()) then kill_dummy (simpl true a) else simpl false a
 
-(*S Special treatment of non-mutual fixpoint for pretty-printing purpose. *)
+(*S Special treatment of fixpoint for pretty-printing purpose. *)
 
-(* TODO a reecrire plus proprement!! *)
-
-let make_general_fix f ids n args m c = 
+let general_optimize_fix f ids n args m c = 
   let v = Array.make n 0 in 
   for i=0 to (n-1) do v.(i)<-i done;
   let aux i = function 
@@ -597,16 +609,16 @@ let optimize_fix a =
     else match a' with 
       | MLfix(_,[|f|],[|c|]) ->
 	  let new_f = MLapp (MLrel (n+1),eta_args n) in 
-	  let new_c = named_lams ids (ml_subst new_f c)
+	  let new_c = named_lams ids (normalize (ml_subst new_f c))
 	  in MLfix(0,[|f|],[|new_c|])
       | MLapp(a',args) ->
 	  let m = List.length args in 
 	  (match a' with 
-	     | MLfix(_,[|_|],[|_|]) when 
+	     | MLfix(_,_,_) when 
 		 (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') 
 		 -> a'
 	     | MLfix(_,[|f|],[|c|]) -> 
-		 (try make_general_fix f ids n args m c
+		 (try general_optimize_fix f ids n args m c
 		  with Impossible -> 
 		    named_lams ids (MLapp (MLfix (0,[|f|],[|c|]),args))) 
 	     | _ -> a)
@@ -764,6 +776,10 @@ let subst_glob_decl r m = function
   | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
+let inline_glob r t l = 
+  if not (inline r t) then true, l 
+  else false, List.map (subst_glob_decl r t) l
+
 let print_ml_decl prm (r,_) = 
   not (to_inline r) || List.mem r prm.to_appear
 
@@ -773,21 +789,54 @@ let add_ml_decls prm decls =
   let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
   (List.rev l @ decls)
 
+let rec expunge_fix_decls prm v c b = function 
+  | [] -> b, [] 
+  | Dglob (r, t) :: l when array_exists ((=) r) v -> 
+      let t = optimize_fix (normalize t) in 
+      (match t with 
+	 | MLfix(_,_,c') when c=c' -> 
+	     let b',l = inline_glob r t l in 
+	     expunge_fix_decls prm v c (b || b' || List.mem r prm.to_appear) l 
+	 | _ -> raise Impossible)
+  | d::l -> let b,l = expunge_fix_decls prm v c b l in b, d::l  
+
 let rec optimize prm = function
   | [] -> 
       []
-  | ( Dabbrev (r,_,Tarity) |
-	Dabbrev(r,_,Tprop) | 
-	  Dglob(r,MLarity) | 
-	    Dglob(r,MLprop) ) as d :: l ->
+  | (Dabbrev (r,_,Tdummy) | Dglob(r,MLdummy)) as d :: l ->
       if List.mem r prm.to_appear then d :: (optimize prm l) 
       else optimize prm l
   | Dglob (r,t) :: l ->
-      let t = normalize t in
-      let b = not (inline r t) in
-      let l = if b then l else List.map (subst_glob_decl r t) l in
-      if (b || prm.modular || List.mem r prm.to_appear) then 
-	Dglob (r,optimize_fix t) :: (optimize prm l)
-      else 
-	optimize prm l
+      let t = optimize_fix (normalize t) in
+      (try optimize_Dfix prm r t l 
+      with Impossible -> 
+	let b,l = inline_glob r t l in 
+	if (b || prm.modular || List.mem r prm.to_appear) then 
+	  Dglob (r,t) :: (optimize prm l)
+	else optimize prm l)
   | d :: l -> d :: (optimize prm l)
+
+and optimize_Dfix prm r t l = 
+  match t with 
+    | MLfix (_, f, c) -> 
+	let b = not (inline r t) in 
+	let l = if b then l else List.map (subst_glob_decl r t) l in
+	if Array.length f = 1 then 
+	  if b then 
+	    Dfix ([|r|], c) :: (optimize prm l)
+	  else optimize prm l
+	else 
+	  let v = try 
+	    let d = dirpath (sp_of_r r) in 
+	    Array.map (fun id -> locate (make_qualid d id)) f 
+	  with Not_found -> raise Impossible 
+	  in 
+	  let b,l = expunge_fix_decls prm v c (prm.modular || b) l in 
+	  if b then Dfix (v, c) :: (optimize prm l)
+	  else optimize prm l 
+    | _ -> raise Impossible
+
+
+
+
+
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index b58ee5260c..f9d1fb4f46 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -13,11 +13,11 @@ open Term
 open Miniml
 open Nametab
 
-(*s Special identifiers. [prop_name] is to be used for propositions
+(*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
 
 val anonymous : identifier
-val prop_name : identifier
+val dummy_name : identifier
 val flex_name : identifier
 val id_of_name : name -> identifier
 
@@ -34,7 +34,7 @@ val nb_lams : ml_ast -> int
 
 val anonym_lams : ml_ast -> int -> ml_ast
 
-val prop_lams : ml_ast -> int -> ml_ast
+val dummy_lams : ml_ast -> int -> ml_ast
 
 val named_lams : identifier list -> ml_ast -> ml_ast
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index e785499b4b..78221b1be8 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -84,8 +84,8 @@ type env = identifier list * Idset.t
 let rec rename_vars avoid = function
   | [] -> 
       [], avoid
-  | id :: idl when id == prop_name ->
-      (* we don't rename propositions binders *)
+  | id :: idl when id == dummy_name ->
+      (* we don't rename dummy binders *)
       let (idl', avoid') = rename_vars avoid idl in
       (id :: idl', avoid')
   | id :: idl ->
@@ -114,15 +114,13 @@ let keywords =
     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "prop" ; "arity" ] 
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "dummy" ] 
   Idset.empty
 
-let preamble _ used_modules used_prop = 
-  (if used_prop then 
-    str "type prop = unit" ++ fnl () ++
-    str "let prop = ()" ++ fnl () ++ fnl () ++
-    str "type arity = unit" ++ fnl () ++
-    str "let arity = ()" ++ fnl () ++ fnl ()
+let preamble _ used_modules used_dummy = 
+  (if used_dummy then 
+    str "type dummy = unit" ++ fnl () ++
+    str "let dummy = ()" ++ fnl () ++ fnl ()
   else mt ())
   ++
   Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl())
@@ -158,8 +156,7 @@ let rec pp_type par ren t =
 	(open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ 
 	   pp_rec false t2 ++ close_par par)
     | Tglob r -> pp_type_global r
-    | Tprop -> str "prop"
-    | Tarity -> str "arity"
+    | Tdummy -> str "dummy"
   in 
   hov 0 (pp_rec par t)
 
@@ -254,10 +251,8 @@ let rec pp_expr par env args =
 	(* An [MLexn] may be applied, but I don't really care. *)
 	(open_par par ++ str "assert false" ++ spc () ++ 
 	 str ("(* "^s^" *)") ++ close_par par)
-    | MLprop ->
-	str "prop" (* An [MLprop] may be applied, but I don't really care. *)
-    | MLarity ->
-	str "arity" (* idem for [MLarity]. *)
+    | MLdummy ->
+	str "dummy" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) ->
 	let tvars = get_tvars t in 
 	let _,ren = rename_tvars keywords tvars in 
@@ -346,7 +341,6 @@ let pp_one_ind prefix (pl,name,cl) =
 		      (fun () -> (spc () ++ str "* ")) (pp_type true ren) l))
   in
   (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ 
-   (* TODO: possible clash with Coq unit *)
    if cl = [] then str " unit (* empty inductive *)" 
    else (fnl () ++
 	 v 0 (str "    " ++
@@ -388,10 +382,10 @@ let pp_decl = function
       hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
 	       pp_type_global r ++ spc () ++ str "=" ++ spc () ++ 
 	       pp_type false ren t ++ fnl ())
-  | Dglob (r, MLfix (_,[|_|],[|def|])) ->
-      let id = rename_global r in
-      let env' = [id], P.globals() in
-      (hov 2 (pp_fix false env' None ([|id|],[|def|]) []))
+  | Dfix (rv, defs) ->
+      let ids = Array.map rename_global rv in 
+      let env = List.rev (Array.to_list ids), P.globals() in
+      (hov 2 (pp_fix false env None (ids,defs) []))
   | Dglob (r, a) ->
       hov 0 (str "let " ++ 
 	       pp_function (empty_env ()) (pp_global' r) a ++ fnl ())