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 ++++----
 interp/constrintern.mli | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'interp')

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
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d33d43345..4d2c994679 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -157,7 +157,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?global_level:bool -> ?impl_env:internalization_env ->
+  ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map ref -> local_binder list ->
   internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
-- 
cgit v1.2.3