Merge PR #15456: Fixes #15455: regression due to #14606 in computing …

…best implicit arguments signature for projections Reviewed-by: SkySkimmer Ack-by: artagnon Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
coq · Jan 10, 2022 · 19d68a0 · 19d68a0
2 parents bd6cead + 2294acd
commit 19d68a0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/interp/impargs.ml b/interp/impargs.ml
@@ -792,7 +792,7 @@ let select_impargs_size_for_proj ~nexpectedparams ~ngivenparams ~nextraargs impl
     (* Force the main argument to be explicit *)
     (nimps1, imps1 @ [None], imps2)
   in
-  let nallgivenargs = ngivenparams + nextraargs in
+  let nallgivenargs = ngivenparams + nextraargs + 1 in
   let little_enough_all_implicit = function
   | (DefaultImpArgs, impls) -> Some (split_implicit_params impls)
   | (LessArgsThan r, impls) when nallgivenargs <= r -> Some (split_implicit_params impls)

diff --git a/test-suite/bugs/bug_15455.v b/test-suite/bugs/bug_15455.v
@@ -0,0 +1,5 @@
+(* A reduced form of bug #15455 *)
+
+Record R := { f {Hp : 0 = 0} (Hq : 0 = 0) : bool }.
+Arguments f _ Hp Hq, _ {Hp} Hq.
+Check fun x => x.(f) eq_refl eq_refl.