diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-01 13:53:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-01 13:53:45 +0000 |
| commit | d68d100a90556b99d4639b2909d1028cbe8db8e2 (patch) | |
| tree | 0d6ed2c423ce7c3bd0760088203b84720751f7da /contrib/extraction | |
| parent | c482258b332a27c38ec0547d3c36e9f04eeae9c2 (diff) | |
reparation bug #1128
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8886 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/mlutil.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index bfff12ef9..aa74b6cea 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -981,7 +981,8 @@ let general_optimize_fix f ids n args m c = let v = Array.make n 0 in for i=0 to (n-1) do v.(i)<-i done; let aux i = function - | MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1) + | MLrel j when v.(j-1)>=0 -> + if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1) | _ -> raise Impossible in list_iter_i aux args; let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in @@ -1008,8 +1009,7 @@ let optimize_fix a = -> a' | MLfix(_,[|f|],[|c|]) -> (try general_optimize_fix f ids n args m c - with Impossible -> - named_lams ids (MLapp (MLfix (0,[|f|],[|c|]),args))) + with Impossible -> a) | _ -> a) | _ -> a |