diff options
| author | Gaëtan Gilbert | 2020-07-07 14:25:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 11:12:44 +0100 |
| commit | 9990bea3e163850c0ac4dca982c73d2b2bc19a38 (patch) | |
| tree | 28d9ddc1dec90446dbbbcfb448dcce80862431a8 /vernac/comInductive.ml | |
| parent | 779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff) | |
Infrastructure for cumulative inductive syntax (no grammar extension yet)
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index bb26ce652e..6b37958ab3 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -367,6 +367,12 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars +let variance_of_entry ~cumulative = function + | Monomorphic_entry _ -> None + | Polymorphic_entry (nas,_) -> + Some (Array.map (fun _ -> None) nas) +(* TODO syntax to have non-None elements *) + let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in @@ -429,7 +435,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; mind_entry_template = is_template; - mind_entry_cumulative = poly && cumulative; + mind_entry_variance = variance_of_entry ~cumulative uctx; } in mind_ent, Evd.universe_binders sigma |