Refonte complete de la génération des types ML

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

1 files changed, 0 insertions, 22 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 7bb9402d4..d4941008a 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -39,16 +39,6 @@ let id_of_name = function
 
 (*S Operations upon ML types. *)
 
-(*s Get all type variables from a ML type *)
-
-let get_tvars t = 
-  let rec get_rec s = function 
-  | Tvar i -> Idset.add i s
-  | Tapp l -> List.fold_left get_rec s l 
-  | Tarr (a,b) -> get_rec (get_rec s a) b
-  | a -> s
-  in Idset.elements (get_rec Idset.empty t)
-
 (*s Does a section path occur in a ML type ? *)
 
 let sp_of_r r = match r with 
@@ -63,18 +53,6 @@ let rec type_mem_sp sp = function
   | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b)
   | _ -> false
 
-(*s In an ML type, update the arguments to all inductive types [(sp,_)] *)  
-
-let rec update_args sp vl = function  
-  | Tapp ( Tglob r :: l ) -> 
-      (match r with 
-	| IndRef (s,_) when s = sp -> Tapp ( Tglob r :: l @ vl )
-	| _ -> Tapp (Tglob r :: (List.map (update_args sp vl) l)))
-  | Tapp l -> Tapp (List.map (update_args sp vl) l) 
-  | Tarr (a,b)-> 
-      Tarr (update_args sp vl a, update_args sp vl b)
-  | a -> a
-  
 (*S Generic functions over ML ast terms. *)
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care