From 0f403373e6ecc1be806b9c29812f5c9f48c321de Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 9 Oct 2020 17:32:44 +0000
Subject: Fixes/enhancements with local definitions in records.

Fixes implicit arguments from the body of a defined field not taken into account.
Get (a bit) more information for detection of SProp relevance in
implicitly-typed defined field. (It should be done at the very end of
the inference phase, though, because some evars may not yet be
instantiated.)
---
 test-suite/success/Record.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite')

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;
+ }.
-- 
cgit v1.2.3