1 files changed, 6 insertions, 13 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index afee2a5868..9bbfb8eec6 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -162,7 +162,7 @@ let interp_cstrs env sigma impls mldata arity ind =
   let sigma, (ctyps'', cimpls) =
     on_snd List.split @@
     List.fold_left_map (fun sigma l ->
-        interp_type_evars_impls env sigma ~impls l) sigma ctyps' in
+        interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in
   sigma, (cnames, ctyps'', cimpls)
 
 let sign_level env evd sign =
@@ -358,9 +358,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   then user_err (str "Inductives with uniform parameters may not have attached notations.");
   let sigma, udecl = interp_univ_decl_opt env0 udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
-    interp_context_evars env0 sigma uparamsl in
+    interp_context_evars ~program_mode:false env0 sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
-    interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl
+    interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -457,15 +457,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
         indimpls, List.map (fun impls ->
           userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
-  let univs =
-    match uctx with
-    | Polymorphic_const_entry (nas, uctx) ->
-      if cum then
-        Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
-      else Polymorphic_ind_entry (nas, uctx)
-    | Monomorphic_const_entry uctx ->
-      Monomorphic_ind_entry uctx
-  in
+  let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -473,7 +465,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       mind_entry_finite = finite;
       mind_entry_inds = entries;
       mind_entry_private = if prv then Some false else None;
-      mind_entry_universes = univs;
+      mind_entry_universes = uctx;
+      mind_entry_variance = variance;
     }
   in
   (if poly && cum then