diff options
| author | Hugo Herbelin | 2020-10-09 17:32:44 +0000 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-16 01:29:19 +0200 |
| commit | 0f403373e6ecc1be806b9c29812f5c9f48c321de (patch) | |
| tree | 5537154ba078467d8932787ed4b07417f9238481 /stm | |
| parent | 12ea3318943f2a47f45d939aa206acc263a6341d (diff) | |
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.)
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |