diff options
| author | Pierre-Marie Pédrot | 2019-02-05 15:53:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 15:53:55 +0100 |
| commit | 38b1682ee6b6342ca582bac4e658f7d1c3919de4 (patch) | |
| tree | c22a2690095ed66a086ebf6848e039c4ef4b7620 /kernel/environ.mli | |
| parent | 9d3394cbc37be3ad8b4fbd32d32c193a55368196 (diff) | |
| parent | f7148d56b17ee7d06cac26392c85f3b8c7cbd974 (diff) | |
Merge PR #9438: Cleanup universe length for inductives in vconv
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 8d5bd85b94..a9e0717559 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -246,6 +246,10 @@ val add_mind : MutInd.t -> mutual_inductive_body -> env -> env raises [Not_found] if the required path is not found *) val lookup_mind : MutInd.t -> env -> mutual_inductive_body +(** The universe context associated to the inductive, empty if not + polymorphic *) +val mind_context : env -> MutInd.t -> Univ.AUContext.t + (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool val polymorphic_pind : pinductive -> env -> bool |