diff options
| author | Gaëtan Gilbert | 2017-11-10 15:05:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-11 22:28:39 +0100 |
| commit | 6c2d10b93b819f0735a43453c78566795de8ba5a (patch) | |
| tree | 14dffe59d0edfacf547b3912352f14420df047b8 /pretyping/pretyping.mllib | |
| 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 'pretyping/pretyping.mllib')
| -rw-r--r-- | pretyping/pretyping.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 1da5b4567f..ae4ad0be7d 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,6 +4,7 @@ Locusops Pretype_errors Reductionops Inductiveops +InferCumulativity Vnorm Arguments_renaming Nativenorm |