From f19d0c7baf91fb410de77baed391b0a16db9c4e2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 May 2015 11:33:59 +0200
Subject: Fixing computation of implicit arguments by position in fixpoints
 (#4217).

---
 interp/constrintern.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8f0d56c5bd..982d9bfe39 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1893,7 +1893,7 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err_loc (loc,"internalize", explain_internalization_error e)
 
-let interp_rawcontext_evars env evdref bl =
+let interp_rawcontext_evars env evdref k bl =
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
@@ -1914,11 +1914,11 @@ let interp_rawcontext_evars env evdref bl =
 	      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, n, impls))
-      (env,[],1,[]) (List.rev bl)
+      (env,[],k+1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_rawcontext_evars env evdref bl in
+  let x = interp_rawcontext_evars env evdref shift bl in
   int_env, x
 
-- 
cgit v1.2.3