diff options
| author | letouzey | 2004-02-13 16:06:25 +0000 |
|---|---|---|
| committer | letouzey | 2004-02-13 16:06:25 +0000 |
| commit | 61f6841c55ec034982d29f6bcaf7b51df21ca88a (patch) | |
| tree | 75a200ce80e403c7ff8522b13fc14b1a0d8efb69 | |
| 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
| -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 bf1b200f07..e60765b7e1 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 |