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 /vernac/vernacentries.ml | |
| 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 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0d3f38d139..3ced38d6ea 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -700,7 +700,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records = if Dumpglob.dump () then let () = Dumpglob.dump_definition id false "rec" in let iter (x, _) = match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) -> Dumpglob.dump_definition (make ?loc id) false "proj" | _ -> () in @@ -777,7 +777,7 @@ let vernac_inductive ~atts kind indl = in let (coe, (lid, ce)) = l in let coe' = if coe then BackInstance else NoInstance in - let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), + let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce), { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then |