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.)
---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 3996c64b67..ffae2866c0 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -128,7 +128,7 @@ let classify_vernac e =
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
-            | AssumExpr({v=Names.Name n},_), _ -> Some n
+            | AssumExpr({v=Names.Name n},_,_), _ -> Some n
             | _ -> None) l) l in
         VtSideff (List.flatten ids, VtLater)
     | VernacScheme l ->
-- 
cgit v1.2.3