Merge #291

291: Adapt to coq/coq#12653 (syntax for cumulative inductives) r=Janno a=SkySkimmer Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Mtac2 · Nov 18, 2020 · 6ff46f8 · 6ff46f8
2 parents 71b4b58 + ffaedda
commit 6ff46f8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/run.ml b/src/run.ml
@@ -1207,7 +1207,7 @@ let declare_mind env sigma params sigs mut_constrs =
              mind_entry_params;
              mind_entry_universes=Evd.univ_entry ~poly:false sigma;
              mind_entry_template;
-             mind_entry_cumulative=false;
+             mind_entry_variance=None;
              mind_entry_private=None;
             } UnivNames.empty_binders [] in
   (sigma, CoqUnit.mkTT)