From 78fe03354fa44a18edbad853ed65a7ba0c3ce6e4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 25 May 2001 12:22:21 +0000
Subject: Oups: flingait les Dglob dans optimize

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1764 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/mlutil.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 6413e1ec47..19e0a9ade7 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -393,17 +393,18 @@ let rec optimize prm = function
       let l' = List.map (expand (id,t)) l in optimize prm l'
   i*)	    
   | Dglob (r,t) :: l ->
-      let t' = normalize t in
-      let l' = if expand prm r t' then 
+      let t = normalize t in
+      let b = expand prm r t in
+      let l = if b then 
 	begin
 	  if_verbose warning_expansion r;
-	  List.map (subst_glob_decl r t') l
+	  List.map (subst_glob_decl r t) l
 	end
       else l in 
-      if prm.modular || l' = [] then 
-	Dglob (r,t') :: (optimize prm l')
+      if prm.modular || l = [] || not b then 
+	Dglob (r,t) :: (optimize prm l)
       else
-	optimize prm l'
+	optimize prm l
 
 
 (*s Table for direct ML extractions. *)
-- 
cgit v1.2.3