Merge branch 'beforepoly' of /Users/mat/research/coq/git into trunk

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.
 

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

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

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