interp_context_evars: removed unused [shift] argument

Became unused in e034b4090ca45410853db60ae2a5d2f220b48792

3 files changed, 12 insertions, 11 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))
 
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 564d24c1ea..78572c6aa6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -110,7 +110,7 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
     else [], fix.Vernacexpr.binders in
   let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
   let sigma, (impl_env', ((env'', ctx'), imps')) =
-    interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
+    interp_context_evars ~program_mode ~impl_env env' sigma after
   in
   let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)