diff --git a/template-rocq/src/quoter.ml b/template-rocq/src/quoter.ml
index 5064c66f1..9d2c34bd8 100644
--- a/template-rocq/src/quoter.ml
+++ b/template-rocq/src/quoter.ml
@@ -464,7 +464,13 @@ struct
       let nparams = Q.quote_int mib.Declarations.mind_nparams in
       let paramsctx, acc = quote_rel_context quote_term acc env sigma mib.Declarations.mind_params_ctxt in
       let uctx = quote_universes_decl mib.Declarations.mind_universes mib.Declarations.mind_template in
-      let var = Option.map (CArray.map_to_list Q.quote_variance) mib.Declarations.mind_variance in
+      let var = match mib.Declarations.mind_variance with
+        | None -> None
+        | Some (qv,uv) ->
+          if not @@ CArray.is_empty qv then CErrors.user_err Pp.(str "Cumulative sort polymorphism not supported.");
+          Some uv
+      in
+      let var = Option.map (CArray.map_to_list Q.quote_variance) var in
       let bodies = List.map Q.mk_one_inductive_body (List.rev ls) in
       let finite = Q.quote_mind_finiteness mib.Declarations.mind_finite in
       (* let templatePoly = Q.quote_bool mi.mind_template in *)
diff --git a/template-rocq/src/run_template_monad.ml b/template-rocq/src/run_template_monad.ml
index 9ec3e4a12..88b5fdc2f 100644
--- a/template-rocq/src/run_template_monad.ml
+++ b/template-rocq/src/run_template_monad.ml
@@ -278,7 +278,7 @@ let unquote_mutual_inductive_entry env evm trm (* of type mutual_inductive_entry
        let evm, univs = denote_universes_entry env evm univs in
        let template = unquote_bool template in
        let variance = unquote_map_option
-           (fun v -> CArray.map_of_list (unquote_map_option unquote_variance) (unquote_list v))
+           (fun v -> [||], CArray.map_of_list (unquote_map_option unquote_variance) (unquote_list v))
            variance
        in
        let priv = unquote_map_option unquote_bool priv in