diff options
| author | Hugo Herbelin | 2014-06-17 13:16:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-17 16:06:41 +0200 |
| commit | 1894f56849f01dbaf7c1fafed5c9b4f26ff6d2e5 (patch) | |
| tree | a6ae8bccb04d556ec8682aa7d7d70c38a6c80c3e /interp | |
| parent | d4a0f7af3b55792c548fae6e47eeef0925ee6e23 (diff) | |
Fixing #3282 (two bugs in the presence of let-in's in "fix").
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 93feb8b460..dc1db3c2b9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1363,7 +1363,7 @@ let internalize globalenv env allow_patvar lvar c = let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.length rbefore) n in + let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = |