diff options
| author | Gaëtan Gilbert | 2019-01-30 12:59:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-30 13:01:55 +0100 |
| commit | f7148d56b17ee7d06cac26392c85f3b8c7cbd974 (patch) | |
| tree | 9c9dc8427d4e4ccf766d941efa1e80b217f89b1c /kernel/environ.ml | |
| parent | a9b141469fe3036355be95d8cf5f0bf5c240fe37 (diff) | |
Cleanup universe length for inductives in vconv
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 77820a301e..5d49609f35 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 |