From 7d261ef454e918c70b8fff1dd10bbe0fbdcb57a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 15:54:26 +0200
Subject: Fixing #3376 and #4191 (wrong index of maximally-inserted implicit
 argument in the presence of let-ins).

---
 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 5151d2a10a..8f0d56c5bd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1913,7 +1913,7 @@ let interp_rawcontext_evars env evdref bl =
 	  | Some b ->
 	      let c = understand_judgment_tcc env evdref b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env, d::params, succ n, impls))
+		(push_rel d env, d::params, n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-- 
cgit v1.2.3