Fixing several wrong computations of implicit arguments by position

in the presence of let-ins.

3 files changed, 10 insertions, 4 deletions

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f702aa62f1..f07773f8bd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -21,3 +21,9 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
 (* Test sharing information between different hypotheses *)
 
 Parameters (a:_) (b:a=0).
+
+(* These examples were failing due to a lifting wrongly taking let-in into account *)
+
+Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
+
+Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
diff --git a/vernac/command.ml b/vernac/command.ml
index f31fce8859..c24dbdf7c0 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl p red_option c ctypopt =
   let ctx = Evd.make_evar_universe_context env pl in
   let evdref = ref (Evd.from_ctx ctx) in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
-  let nb_args = List.length ctx in
+  let nb_args = Context.Rel.nhyps ctx in
   let imps,pl,ce =
     match ctypopt with
       None ->
@@ -838,7 +838,7 @@ type structured_fixpoint_expr = {
 let interp_fix_context env evdref isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
   let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
@@ -1100,7 +1100,7 @@ let interp_recursive isfix fixl notations =
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
   let fiximps = List.map3
-    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
+    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
     fixctximps fixcclimps fixctxs in
   let rec_sign =
     List.fold_left2
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e7d1919ce0..430d48bc76 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'))))
+       (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in