From bacbd175ee22a81f170cc08959d1841847505c6d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 25 Aug 2020 12:32:41 +0200
Subject: Fix incorrect debruijn handling when Record calls
 maybe_unify_params_in

Fix #12887
---
 vernac/record.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/record.ml')

diff --git a/vernac/record.ml b/vernac/record.ml
index d0036e40f9..bd5b71cd6b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -81,12 +81,12 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
          (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
       (env, sigma, [], [], impls_env) nots l
   in
-  let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) ->
+  let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
       let sigma = RelDecl.fold_constr (fun c sigma ->
-          ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c)
+          ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c)
           f sigma
       in
-      EConstr.push_rel f env, sigma)
+      EConstr.push_rel f env, k+1, sigma)
       newfs
   in
   sigma, (impls, newfs)
-- 
cgit v1.2.3