diff options
author | 2017-11-10 15:05:21 +0100 | |
---|---|---|
committer | 2018-02-11 22:28:39 +0100 | |
commit | 6c2d10b93b819f0735a43453c78566795de8ba5a (patch) | |
tree | 14dffe59d0edfacf547b3912352f14420df047b8 /vernac/record.ml | |
parent | 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 (diff) |
Use specialized function for inductive subtyping inference.
This ensures by construction that we never infer constraints outside
the variance model.
Diffstat (limited to 'vernac/record.ml')
-rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 6e35ac4db..d9af5378f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,7 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t mind_entry_universes = univs; } in - let mie = Inductiveops.infer_inductive_subtyping (Global.env ()) mie in + let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in |