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.

3 files changed, 21 insertions, 26 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 56ff757e1a..5cf2b680ca 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -353,7 +353,7 @@ 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 interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+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
   let nf = Evarutil.nf_evars_universes sigma in
@@ -403,7 +403,6 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~
       })
       indnames arities arityconcl constructors
   in
-  let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -412,12 +411,10 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~
       mind_entry_inds = entries;
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
-      mind_entry_variance = variance;
+      mind_entry_cumulative = poly && cumulative;
     }
   in
-  (if poly && cumulative then
-      InferCumulativity.infer_inductive env_ar mind_ent
-   else mind_ent), Evd.universe_binders sigma
+  mind_ent, Evd.universe_binders sigma
 
 let interp_params env udecl uparamsl paramsl =
   let sigma, udecl = interp_univ_decl_opt env udecl in
@@ -504,7 +501,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
         indimpls, List.map (fun impls ->
             userimpls @ impls) cimpls) indimpls constructors
   in
-  let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+  let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
   (mie, pl, impls)
 
 
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 73d385dec8..418d971558 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -49,22 +49,22 @@ val declare_mutual_inductive_with_eliminations
   -> Names.MutInd.t
   [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
 
-val interp_mutual_inductive_constr :
-  sigma:Evd.evar_map ->
-  template:bool option ->
-  udecl:UState.universe_decl ->
-  env_ar:Environ.env ->
-  ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list ->
-  indnames:Names.Id.t list ->
-  arities:EConstr.t list ->
-  arityconcl:(bool * EConstr.ESorts.t) option list ->
-  constructors:(Names.Id.t list * Constr.constr list * 'a list list) list ->
-  env_ar_params:Environ.env ->
-  cumulative:bool ->
-  poly:bool ->
-  private_ind:bool ->
-  finite:Declarations.recursivity_kind ->
-  Entries.mutual_inductive_entry * UnivNames.universe_binders
+val interp_mutual_inductive_constr
+  : sigma:Evd.evar_map
+  -> template:bool option
+  -> udecl:UState.universe_decl
+  -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
+  -> indnames:Names.Id.t list
+  -> arities:EConstr.t list
+  -> arityconcl:(bool * EConstr.ESorts.t) option list
+  -> constructors:(Names.Id.t list * Constr.constr list * 'a list list) list
+  -> env_ar_params:Environ.env
+  (** Environment with the inductives and parameters in the rel_context *)
+  -> cumulative:bool
+  -> poly:bool
+  -> private_ind:bool
+  -> finite:Declarations.recursivity_kind
+  -> Entries.mutual_inductive_entry * UnivNames.universe_binders
 
 (************************************************************************)
 (** Internal API, exported for Record                                   *)
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