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.ml | |
| 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.ml')
| -rw-r--r-- | kernel/environ.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 02f38e7214..886d6b1feb 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -222,6 +222,10 @@ let lookup_constant kn env = let lookup_mind kn env = fst (Mindmap_env.find kn env.env_globals.env_inductives) +let mind_context env mind = + let mib = lookup_mind mind env in + Declareops.inductive_polymorphic_context mib + let lookup_mind_key kn env = Mindmap_env.find kn env.env_globals.env_inductives |