travail sur les types extraits

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

1 files changed, 10 insertions, 9 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index b8764d85d0..c55d3746f7 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -209,7 +209,7 @@ end
 (*s Does a section path occur in a ML type ? *)
 
 let rec type_mem_kn kn = function 
-  | Tmeta _ -> assert false
+  | Tmeta {contents = Some t} -> type_mem_kn kn t
   | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
   | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
@@ -218,7 +218,7 @@ let rec type_mem_kn kn = function
 
 let type_maxvar t = 
   let rec parse n = function 
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> parse n t
     | Tvar i -> max i n 
     | Tarr (a,b) -> parse (parse n a) b
     | Tglob (_,l) -> List.fold_left parse n l 
@@ -228,7 +228,7 @@ let type_maxvar t =
 (*s From [a -> b -> c] to [[a;b],c]. *) 
 
 let rec type_decomp = function 
-  | Tmeta _ -> assert false
+  | Tmeta {contents = Some t} -> type_decomp t 
   | Tarr (a,b) -> let l,h = type_decomp b in a::l, h 
   | a -> [],a
 
@@ -241,7 +241,7 @@ let rec type_recomp (l,t) = match l with
 (*s Translating [Tvar] to [Tvar'] to avoid clash. *)
 
 let rec var2var' = function 
-  | Tmeta _ -> assert false
+  | Tmeta {contents = Some t} -> var2var' t
   | Tvar i -> Tvar' i
   | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
   | Tglob (r,l) -> Tglob (r, List.map var2var' l)
@@ -252,16 +252,17 @@ type abbrev_map = global_reference -> ml_type option
 (*s Delta-reduction of type constants everywhere in a ML type [t].
    [env] is a function of type [ml_type_env]. *)
 
+
 let type_expand env t = 
   let rec expand = function
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> expand t
     | Tglob (r,l) as t ->    
 	(match env r with 
 	   | Some mlt -> expand (type_subst_list l mlt) 
 	   | None -> Tglob (r, List.map expand l))
     | Tarr (a,b) -> Tarr (expand a, expand b)
     | a -> a
-  in expand t
+  in if Table.type_expand () then expand t else t
 
 (*s Idem, but only at the top level of implications. *)
 
@@ -269,7 +270,7 @@ let is_arrow = function Tarr _ -> true | _ -> false
 
 let type_weak_expand env t = 
   let rec expand = function
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> expand t
     | Tglob (r,l) as t ->    
 	(match env r with 
 	   | Some mlt -> 
@@ -290,7 +291,7 @@ let type_neq env t t' = (type_expand env t <> type_expand env t')
 
 let type_to_sign env t = 
   let rec f = function 
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> f t 
     | Tarr (a,b) -> (Tdummy <> a) :: (f b)
     | _ -> [] 
   in f (type_expand env t)
@@ -304,7 +305,7 @@ let type_expunge env t =
     let rec f t s = 
       if List.mem false s then 
 	match t with 
-	  | Tmeta _ -> assert false
+	  | Tmeta {contents = Some t} -> f t s
 	  | Tarr (a,b) -> 
 	      let t = f b (List.tl s) in 
 	      if List.hd s then Tarr (a, t) else t