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/comInductive.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comInductive.mli')

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9c876787a3..91e8f609d5 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -81,8 +81,8 @@ val template_polymorphism_candidate
    monomorphic universe context that can be made parametric in its
    conclusion sort, if one is given. *)
 
-val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int
+val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int
   -> EConstr.t -> Evd.evar_map
 (** [nparams] is the number of parameters which aren't treated as
     uniform, ie the length of params (including letins) where the env
-    is [uniform params, inductives, params]. *)
+    is [uniform params, inductives, params, binders]. *)
-- 
cgit v1.2.3