diff options
author | 2004-02-13 16:06:25 +0000 | |
---|---|---|
committer | 2004-02-13 16:06:25 +0000 | |
commit | 61f6841c55ec034982d29f6bcaf7b51df21ca88a (patch) | |
tree | 75a200ce80e403c7ff8522b13fc14b1a0d8efb69 /contrib | |
parent | 471bd570c4ab1ab9089a9cc00c16ea72ee7b2b37 (diff) |
petit bug avec Extraction Optimize
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5339 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/extraction/mlutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index bf1b200f0..e60765b7e 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -710,7 +710,7 @@ let rec simpl o = function let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in simpl_case o br (simpl o e) | MLletin(id,c,e) when - (id = dummy_name) || (is_atomic c) || (nb_occur_match e <= 1) -> + (id = dummy_name) || (is_atomic c) || (o && (nb_occur_match e <= 1)) -> simpl o (ast_subst c e) | MLfix(i,ids,c) as t when o -> let n = Array.length ids in |