diff options
| -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 |