diff options
| author | letouzey | 2002-03-20 09:10:16 +0000 |
|---|---|---|
| committer | letouzey | 2002-03-20 09:10:16 +0000 |
| commit | 0c1fd0fa599f972847c0e2ba839c6ce8307eb6b2 (patch) | |
| tree | ddb4fe7b754531bbdc86ed3ebf2873e01f86eaf0 | |
| parent | 83a3896d3a9829f65f8cf19dd34890a1ea4913a9 (diff) | |
reparation du controle de l'apparition des termes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2551 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/mlutil.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 59606dd65d..82fdf467c7 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -813,11 +813,11 @@ let rec optimize prm = function | Dglob (r,t) :: l -> let t = normalize t in let b,l = inline_glob r t l in + let b = b || prm.modular || List.mem r prm.to_appear in let t' = optimize_fix t in (try optimize_Dfix prm r t' b l with Impossible -> - if (b || prm.modular || List.mem r prm.to_appear) then - Dglob (r,t') :: (optimize prm l) + if b then Dglob (r,t') :: (optimize prm l) else optimize prm l) | d :: l -> d :: (optimize prm l) @@ -825,8 +825,7 @@ and optimize_Dfix prm r t b l = match t with | MLfix (_, f, c) -> if Array.length f = 1 then - if b then - Dfix ([|r|], c) :: (optimize prm l) + if b then Dfix ([|r|], c) :: (optimize prm l) else optimize prm l else let v = try @@ -834,7 +833,7 @@ and optimize_Dfix prm r t b l = Array.map (fun id -> locate (make_qualid d id)) f with Not_found -> raise Impossible in - let b,l = expunge_fix_decls prm v c (prm.modular || b) l in + let b,l = expunge_fix_decls prm v c b l in if b then Dfix (v, c) :: (optimize prm l) else optimize prm l | _ -> raise Impossible |