diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-05 14:49:13 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:45:20 +0200 |
| commit | bef2e53ae2286d0a7c61697f7a7a71bfdc0a3c99 (patch) | |
| tree | 22a1a98b2e8a7030542fef9345783a4def8a8f9c /pretyping/inductiveops.mli | |
| parent | d83a4a93202c91095c5528fe4b54c83737e5a151 (diff) | |
Subtyping inference for inductoves and records
Also reinferred after sections discharge
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index bdb6f996b..7d89b1b2b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,3 +199,8 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit + +(* inference of subtyping condition for inductive types *) + +val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry |