diff options
| author | letouzey | 2001-10-01 13:31:10 +0000 |
|---|---|---|
| committer | letouzey | 2001-10-01 13:31:10 +0000 |
| commit | 2c8b6053f569abe11f8fc4c8e6a2ead0a9c65cab (patch) | |
| tree | b8047a87ba04189462d2ae9367c89646ebeaee47 /contrib | |
| parent | bbd32b601943e8864ff3842a2ed2d7ba9d1ecea2 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/mlutil.ml | 10 |
1 files 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' |