Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record types not taken into account

Reviewed-by: SkySkimmer

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index ce07512a1e..beb424dd40 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -93,3 +93,18 @@ Record R : Type := {
 (* This is used in a couple of development such as UniMatch *)
 
 Record S {A:Type} := { a : A; b : forall A:Type, A }.
+
+(* Bug #13165 on implicit arguments in defined fields *)
+Record T := {
+ f {n:nat} (p:n=n) := nat;
+ g := f (eq_refl 0)
+}.
+
+(* Slight improvement in when SProp relevance is detected *)
+Inductive True : SProp := I.
+Inductive eqI : True -> SProp := reflI : eqI I.
+
+Record U (c:True) := {
+ u := c;
+ v := reflI : eqI u;
+ }.