diff options
| author | Gaëtan Gilbert | 2019-10-29 13:50:47 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:52:46 +0100 |
| commit | 4f1d657f42957d0c2d115424564eedf599584cbc (patch) | |
| tree | 7ff261e020f8c5e09720e1a7a5015fd4f1723da2 /vernac/record.ml | |
| parent | b621bc02657bd1effcca371b56260b0a7a327ed9 (diff) | |
Remove variance info from inductive entries, infer in indtyping
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 1ee6812f4e..ea10e06d02 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | Polymorphic_entry (nas, ctx) -> true, Polymorphic_entry (nas, ctx) in - let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -478,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; - mind_entry_variance = variance; + mind_entry_cumulative = poly && cumulative; } in - let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let impls = List.map (fun _ -> paramimpls, []) record_data in let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag |