From 2c8b6053f569abe11f8fc4c8e6a2ead0a9c65cab Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 1 Oct 2001 13:31:10 +0000
Subject: correction de deux petits bugs: case_identité trop fort et Anomaly
 dans le toplevel

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

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index a01fc5bfca..cb555a67a4 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -217,7 +217,9 @@ let check_identity_case br =
 	  if r<>r' then raise Impossible;
 	  check_list (List.length l) l'
       | _ -> raise Impossible
-  in Array.iter check_one_branch br
+  in 
+  if br=[||] then raise Impossible;
+  Array.iter check_one_branch br
 
 
 let check_constant_case br = 
@@ -457,8 +459,10 @@ let rec optimize prm = function
       []
   | (Dtype _ | Dabbrev _) as d :: l -> 
       d :: (optimize prm l)
-  | Dglob (_, MLprop) :: l ->
-      optimize prm l
+  | Dglob (r, MLprop) as d :: l ->
+      if Refset.mem r prm.to_keep then
+	d :: (optimize prm l) 
+      else optimize prm l
   (*i
   | Dglob(id,(MLexn _ as t)) as d :: l ->
       let l' = List.map (expand (id,t)) l in optimize prm l'
-- 
cgit v1.2.3