interp_context_evars: removed unused [shift] argument

Became unused in e034b4090ca45410853db60ae2a5d2f220b48792

2 files changed, 11 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d3b1bbb24..48fb4a4a5d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2530,12 +2530,12 @@ let intern_context env impl_env binders =
               binder_block_names = Some (Some AbsPi,ids)}, []) binders in
   (lenv.impls, List.map glob_local_binder_of_extended bl)
 
-let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
+let interp_glob_context_evars ?(program_mode=false) env sigma bl =
   let open EConstr in
   let flags = { Pretyping.all_no_fail_flags with program_mode } in
-  let env, sigma, par, _, impls =
+  let env, sigma, par, impls =
     List.fold_left
-      (fun (env,sigma,params,n,impls) (na, k, b, t) ->
+      (fun (env,sigma,params,impls) (na, k, b, t) ->
        let t' =
          if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
          else t
@@ -2551,16 +2551,17 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
                 | MaxImplicit -> CAst.make (Some (na,true)) :: impls
                 | Explicit -> CAst.make None :: impls
               in
-                (push_rel d env, sigma, d::params, succ n, impls)
+                (push_rel d env, sigma, d::params, impls)
           | Some b ->
               let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
               let r = Retyping.relevance_of_type env sigma t in
               let d = LocalDef (make_annot na r, c, t) in
-                (push_rel d env, sigma, d::params, n, impls))
-      (env,sigma,[],k+1,[]) (List.rev bl)
-  in sigma, ((env, par), List.rev impls)
+                (push_rel d env, sigma, d::params, impls))
+      (env,sigma,[],[]) (List.rev bl)
+  in
+  sigma, ((env, par), List.rev impls)
 
-let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
+let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params =
   let int_env,bl = intern_context env impl_env params in
-  let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in
+  let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in
   sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2eb96aad56..898a3e09c8 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -156,7 +156,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?program_mode:bool -> ?impl_env:internalization_env -> ?shift:int ->
+  ?program_mode:bool -> ?impl_env:internalization_env ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))