From 1894f56849f01dbaf7c1fafed5c9b4f26ff6d2e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 17 Jun 2014 13:16:42 +0200
Subject: Fixing #3282 (two bugs in the presence of let-in's in "fix").

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

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) =
-- 
cgit v1.2.3