From 21d308fc083ee395e7b1ff78e75ec3a1305cb2f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 2 Apr 2017 19:12:44 +0200
Subject: Fixing several wrong computations of implicit arguments by position
 in the presence of let-ins.

---
 vernac/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/lemmas.ml')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e7d1919ce..430d48bc7 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
-- 
cgit v1.2.3