diff --git a/test-suite/success/indelim.v b/test-suite/success/indelim.v
index 3dd03df5b695..91b6dee2ecef 100644
--- a/test-suite/success/indelim.v
+++ b/test-suite/success/indelim.v
@@ -11,9 +11,6 @@ Inductive False : Prop :=.
 
 Inductive Empty_set : Set :=.
 
-Fail Inductive Large_set : Set :=
-  large_constr : forall A : Set, A -> Large_set.
-
 Fail Inductive Large_set : Set :=
   large_constr : forall A : Set, A -> Large_set.
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d6e5b568a143..6e9ccdc99c2f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -407,8 +407,7 @@ open Autoinstance
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
    or subinstances *)
-let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
-  let poly = Flags.use_polymorphic_flag () in
+let definition_structure (kind,poly,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
diff --git a/toplevel/record.mli b/toplevel/record.mli
index e640028b6fe8..58c9fdd5c296 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -35,6 +35,6 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   identifier * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9c9bdc697e6d..45f0fccf90a4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -525,7 +525,7 @@ let vernac_record k poly finite infer struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,poly,finite,infer,struc,binders,cfs,const,sort))
 
 let vernac_inductive poly finite infer indl =
   if Dumpglob.dump () then