Allow declaring universe constraints at definition level.

Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof.  By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.

Declarations of universe binders and constraints also works for
monomorphic definitions.

34 files changed, 417 insertions, 203 deletions

diff --git a/API/API.ml b/API/API.ml
index 68da858ba..46ad36d36 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -162,6 +162,7 @@ module Indrec = Indrec
 (* module Cases *)
 module Pretyping = Pretyping
 module Unification = Unification
+module Univdecls = Univdecls
 (******************************************************************************)
 (* interp                                                                     *)
 (******************************************************************************)
diff --git a/API/API.mli b/API/API.mli
index 901ed3528..83f4a3c50 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1648,6 +1648,14 @@ sig
   type sort_info = Names.Name.t Loc.located list
   type glob_sort = sort_info glob_sort_gen
 
+  type ('a, 'b) gen_universe_decl = {
+    univdecl_instance : 'a; (* Declared universes *)
+    univdecl_extensible_instance : bool; (* Can new universes be added *)
+    univdecl_constraints : 'b; (* Declared constraints *)
+    univdecl_extensible_constraints : bool (* Can new constraints be added *) }
+
+  type glob_constraint = glob_level * Univ.constraint_type * glob_level
+
   type case_style = Term.case_style =
     | LetStyle
     | IfStyle
@@ -2461,7 +2469,6 @@ sig
        constr_expr list list *
          local_binder_expr list list
 
-  type typeclass_constraint = (Names.Name.t Loc.located * Names.Id.t Loc.located list option) * Decl_kinds.binding_kind * constr_expr
   type constr_pattern_expr = constr_expr
 end
 
@@ -3708,6 +3715,10 @@ sig
 
   type obsolete_locality = bool
 
+  type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl
+
+  type ident_decl = lident * universe_decl_expr option
+
   type lstring
   type 'a with_coercion = coercion_flag * 'a
   type scope_name = string
@@ -3725,9 +3736,7 @@ sig
     | Constructors of constructor_expr list
     | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
 
-  type plident = lident * lident list option
-
-  type inductive_expr = plident with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr
+  type inductive_expr = ident_decl with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr
 
   type syntax_modifier =
     | SetItemLevel of string list * Extend.production_level
@@ -3741,18 +3750,20 @@ sig
 
   type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
 
+  type typeclass_constraint = (Names.Name.t Loc.located * universe_decl_expr option) * Decl_kinds.binding_kind * constr_expr
+
   type definition_expr =
     | ProveBody of local_binder_expr list * constr_expr
     | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
                     * constr_expr option
   type proof_expr =
-    plident option * (local_binder_expr list * constr_expr)
+    ident_decl option * (local_binder_expr list * constr_expr)
 
   type proof_end =
     | Admitted
     | Proved of opacity_flag * lident option
 
-  type fixpoint_expr = plident * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option
+  type fixpoint_expr = ident_decl * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option
 
   type cofixpoint_expr
 
@@ -3831,12 +3842,12 @@ sig
       scope_name option
   | VernacNotationAddFormat of string * string * string
   | VernacDefinition of
-      (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr
+      (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * ident_decl * definition_expr
   | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
-      inline * (plident list * Constrexpr.constr_expr) with_coercion list
+      inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list
   | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
@@ -3860,7 +3871,7 @@ sig
   | VernacInstance of
       bool *
       Constrexpr.local_binder_expr list *
-        Constrexpr.typeclass_constraint *
+        typeclass_constraint *
           (bool * Constrexpr.constr_expr) option *
       hint_info_expr
   | VernacContext of Constrexpr.local_binder_expr list
@@ -3952,7 +3963,7 @@ sig
     | SelectAll
   and vernac_classification = vernac_type * vernac_when
   and one_inductive_expr =
-    plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list
+    ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list
 end
 
 (* XXX: end manual intf move *)
@@ -4089,6 +4100,18 @@ sig
     Environ.env -> Evd.evar_map -> ?flags:unify_flags -> EConstr.constr * EConstr.constr -> Evd.evar_map * EConstr.constr
 end
 
+module Univdecls :
+sig
+  type universe_decl =
+    (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+  val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr ->
+                         Evd.evar_map * universe_decl
+  val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option ->
+                             Evd.evar_map * universe_decl
+  val default_univ_decl : universe_decl
+end
+
 (************************************************************************)
 (* End of modules from pretyping/                                       *)
 (************************************************************************)
@@ -4487,12 +4510,11 @@ sig
 
   type proof_terminator
   type lemma_possible_guards
-  type universe_binders
   type closed_proof = proof_object * proof_terminator
 
   val make_terminator : (proof_ending -> unit) -> proof_terminator
   val start_dependent_proof :
-    Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+    Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
     Proofview.telescope -> proof_terminator -> unit
   val with_current_proof :
     (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a
@@ -5546,7 +5568,7 @@ sig
 
   val mk_hook :
     (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
-  val start_proof : Names.Id.t -> ?pl:Proof_global.universe_binders -> Decl_kinds.goal_kind -> Evd.evar_map ->
+  val start_proof : Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Evd.evar_map ->
     ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
     ?sign:Environ.named_context_val -> EConstr.types ->
     ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
@@ -5622,7 +5644,7 @@ sig
 
   type structured_fixpoint_expr = {
     fix_name : Id.t;
-    fix_univs : lident list option;
+    fix_univs : universe_decl_expr option;
     fix_annot : Id.t Loc.located option;
     fix_binders : local_binder_expr list;
     fix_body : constr_expr option;
@@ -5631,7 +5653,7 @@ sig
 
   type structured_one_inductive_expr = {
     ind_name : Id.t;
-    ind_univs : lident list option;
+    ind_univs : universe_decl_expr option;
     ind_arity : constr_expr;
     ind_lc : (Id.t * constr_expr) list
   }
@@ -5647,7 +5669,7 @@ sig
     (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
     Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit
 
-  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option ->
+  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
     Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
     Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit
 
@@ -5660,7 +5682,7 @@ sig
 
   val interp_fixpoint :
     structured_fixpoint_expr list -> Vernacexpr.decl_notation list ->
-    recursive_preentry * Vernacexpr.lident list option * UState.t *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
       (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
   val extract_mutual_inductive_declaration_components :
@@ -5688,7 +5710,7 @@ sig
     ?refine:bool ->
     Decl_kinds.polymorphic ->
     Constrexpr.local_binder_expr list ->
-    Constrexpr.typeclass_constraint ->
+    Vernacexpr.typeclass_constraint ->
     (bool * Constrexpr.constr_expr) option ->
     ?generalize:bool ->
     ?tac:unit Proofview.tactic  ->
diff --git a/engine/evd.ml b/engine/evd.ml
index cfc9aa635..06b257a9e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -750,6 +750,26 @@ let universe_context_set d = UState.context_set d.universes
 
 let universe_context ?names evd = UState.universe_context ?names evd.universes
 
+open Misctypes
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let check_implication evd cstrs ctx =
+  let uctx = evar_universe_context evd in
+  let gr = UState.initial_graph uctx in
+  let grext = UGraph.merge_constraints cstrs gr in
+  let cstrs' = Univ.UContext.constraints ctx in
+  if UGraph.check_constraints cstrs' grext then ()
+  else CErrors.user_err ~hdr:"check_univ_decl"
+                  (str "Universe constraints are not implied by the ones declared.")
+
+let check_univ_decl evd decl =
+  let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in
+  let pl, ctx = universe_context ?names:pl evd in
+  if not decl.univdecl_extensible_constraints then
+    check_implication evd decl.univdecl_constraints ctx;
+  pl, ctx
+
 let restrict_universe_context evd vars =
   { evd with universes = UState.restrict evd.universes vars }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 3f00a3b0b..76fa69e31 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -552,6 +552,10 @@ val universe_context : ?names:(Id.t located) list -> evar_map ->
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context
 
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 63bd247d5..312502491 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -97,6 +97,8 @@ let subst ctx = ctx.uctx_univ_variables
 
 let ugraph ctx = ctx.uctx_universes
 
+let initial_graph ctx = ctx.uctx_initial_universes
+
 let algebraics ctx = ctx.uctx_univ_algebraic
 
 let constrain_variables diff ctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index d198fbfbe..ba0305869 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst
 val ugraph : t -> UGraph.t
 (** The current graph extended with the local constraints *)
 
+val initial_graph : t -> UGraph.t
+(** The initial graph with just the declarations of new universes. *)
+
 val algebraics : t -> Univ.LSet.t
 (** The subset of unification variables that can be instantiated with algebraic
     universes as they appear in inferred types only. *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 719af43ed..91398d162 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -14,7 +14,7 @@ open Environ
 open Univ
 open Globnames
 
-let pr_with_global_universes l = 
+let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ())))
   with Not_found -> Level.pr l
 
@@ -31,7 +31,7 @@ let universe_binders_of_global ref =
 
 let register_universe_binders ref l =
   universe_binders_table := Refmap.add ref l !universe_binders_table
-		     
+
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 054e43e7c..afcd7a2ed 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -37,7 +37,7 @@ val dump_notation :
   (Constrexpr.notation * Notation.notation_location) Loc.located ->
   Notation_term.scope_name option -> bool -> unit
 val dump_constraint :
-  Constrexpr.typeclass_constraint -> bool -> string -> unit
+  Vernacexpr.typeclass_constraint -> bool -> string -> unit
 
 val dump_string : string -> unit
 
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 413cd9704..8eadafe66 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -132,10 +132,6 @@ and constr_notation_substitution =
     constr_expr list list * (** for recursive notations *)
     local_binder_expr list list (** for binders subexpressions *)
 
-type typeclass_constraint = (Name.t Loc.located * Id.t Loc.located list option) * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
 type constr_pattern_expr = constr_expr
 
 (** Concrete syntax for modules and module types *)
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 807882b42..8b7073143 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -53,6 +53,7 @@ type level_info = Name.t Loc.located option
 
 type glob_sort = sort_info glob_sort_gen
 type glob_level = level_info glob_sort_gen
+type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
 (** A synonym of [Evar.t], also defined in Term *)
 
@@ -136,3 +137,9 @@ type inversion_kind =
   | SimpleInversion
   | FullInversion
   | FullInversionClear
+
+type ('a, 'b) gen_universe_decl = {
+  univdecl_instance : 'a; (* Declared universes *)
+  univdecl_extensible_instance : bool; (* Can new universes be added *)
+  univdecl_constraints : 'b; (* Declared constraints *)
+  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 94e166f92..fa440f8d6 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -166,8 +166,11 @@ type option_ref_value =
   | StringRefValue of string
   | QualidRefValue of reference
 
-(** Identifier and optional list of bound universes. *)						 
-type plident = lident * lident list option
+(** Identifier and optional list of bound universes and constraints. *)
+
+type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
 
 type sort_expr = Sorts.family
 
@@ -177,10 +180,10 @@ type definition_expr =
       * constr_expr option
 
 type fixpoint_expr =
-    plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+    ident_decl * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
-    plident * local_binder_expr list * constr_expr * constr_expr option
+    ident_decl * local_binder_expr list * constr_expr * constr_expr option
 
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
@@ -199,14 +202,18 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
 type inductive_expr =
-  plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
+  ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  plident * local_binder_expr list * constr_expr option * constructor_expr list
+  ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
+
+type typeclass_constraint = (Name.t Loc.located * universe_decl_expr option) * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
 
 type proof_expr =
-  plident option * (local_binder_expr list * constr_expr)
+  ident_decl option * (local_binder_expr list * constr_expr)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
@@ -338,12 +345,12 @@ type vernac_expr =
 
   (* Gallina *)
   | VernacDefinition of
-      (locality option * definition_object_kind) * plident * definition_expr
+      (locality option * definition_object_kind) * ident_decl * definition_expr
   | VernacStartTheoremProof of theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
-      inline * (plident list * constr_expr) with_coercion list
+      inline * (ident_decl list * constr_expr) with_coercion list
   | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
@@ -352,7 +359,7 @@ type vernac_expr =
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
-  | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list
+  | VernacConstraint of glob_constraint list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index de98415cd..d93c2563d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -142,13 +142,13 @@ let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    record_field decl_notation rec_definition pidentref;
+    record_field decl_notation rec_definition pidentref ident_decl;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
+    [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
         l = LIST0
-          [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
+          [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
           (Some id,(bl,c)) ] ->
           VernacStartTheoremProof (thm, (Some id,(bl,c))::l)
       | stre = assumption_token; nl = inline; bl = assum_list ->
@@ -156,7 +156,7 @@ GEXTEND Gram
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
 	  test_plural_form loc kwd bl;
 	  VernacAssumption (stre, nl, bl)
-      | d = def_token; id = pidentref; b = def_body ->
+      | d = def_token; id = ident_decl; b = def_body ->
           VernacDefinition (d, id, b)
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((Some Discharge, Definition), (id, None), b)
@@ -228,13 +228,29 @@ GEXTEND Gram
       | IDENT "Inline" -> DefaultInline
       | -> NoInline] ]
   ;
-  pidentref:
-    [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
-  ;
   univ_constraint:
     [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
 	r = universe_level -> (l, ord, r) ] ]
   ;
+  pidentref:
+    [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
+  ;
+  univ_decl :
+    [ [  "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ];
+         cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
+                ext = [ "+" -> true | -> false ] -> (l',ext)
+              | -> ([], true) ];
+         "}" ->
+         { univdecl_instance = l;
+           univdecl_extensible_instance = ext;
+           univdecl_constraints = fst cs;
+           univdecl_extensible_constraints = snd cs }
+    ] ]
+  ;
+  ident_decl:
+    [ [ i = identref; l = OPT univ_decl -> (i, l)
+  ] ]
+  ;
   finite_token:
     [ [ IDENT "Inductive" -> (Inductive_kw,Finite)
       | IDENT "CoInductive" -> (CoInductive,CoFinite)
@@ -292,7 +308,7 @@ GEXTEND Gram
       | -> RecordDecl (None, []) ] ]
   ;
   inductive_definition:
-    [ [ oc = opt_coercion; id = pidentref; indpar = binders;
+    [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
         c = OPT [ ":"; c = lconstr -> c ];
         lc=opt_constructors_or_fields; ntn = decl_notation ->
 	   (((oc,id),indpar,c,lc),ntn) ] ]
@@ -318,14 +334,14 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = pidentref;
+    [ [ id = ident_decl;
 	bl = binders_fixannot;
         ty = type_cstr;
 	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
 	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = pidentref; bl = binders; ty = type_cstr;
+    [ [ id = ident_decl; bl = binders; ty = type_cstr;
         def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -397,7 +413,7 @@ GEXTEND Gram
     [ [ "("; a = simple_assum_coe; ")" -> a ] ]
   ;
   simple_assum_coe:
-    [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr ->
+    [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
         (not (Option.is_empty oc),(idl,c)) ] ]
   ;
 
@@ -800,7 +816,7 @@ GEXTEND Gram
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
   instance_name:
-    [ [ name = pidentref; sup = OPT binders ->
+    [ [ name = ident_decl; sup = OPT binders ->
 	  (let ((loc,id),l) = name in ((loc, Name id),l)),
           (Option.default [] sup)
       | -> ((Loc.tag ~loc:!@loc Anonymous), None), []  ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 40c5da7a5..3d00b220b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -445,6 +445,7 @@ module Prim =
     let name = Gram.entry_create "Prim.name"
     let identref = Gram.entry_create "Prim.identref"
     let pidentref = Gram.entry_create "Prim.pidentref"
+    let ident_decl = Gram.entry_create "Prim.ident_decl"
     let pattern_ident = Gram.entry_create "pattern_ident"
     let pattern_identref = Gram.entry_create "pattern_identref"
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 4e6bff20a..2f0375419 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -195,6 +195,7 @@ module Prim :
     val name : Name.t located Gram.entry
     val identref : Id.t located Gram.entry
     val pidentref : (Id.t located * (Id.t located list) option) Gram.entry
+    val ident_decl : ident_decl Gram.entry
     val pattern_ident : Id.t Gram.entry
     val pattern_identref : Id.t located Gram.entry
     val base_ident : Id.t Gram.entry
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cf676f598..a8d518fbd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -216,7 +216,6 @@ let interp_prod_item = function
       assert (String.equal s "tactic");
       begin match Tacarg.wit_tactic with
       | ExtraArg tag -> ArgT.Any tag
-      | _ -> assert false
       end
     in
     let symbol = interp_entry_name interp symbol in
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c8b3307d7..d04dcb8e3 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -29,3 +29,4 @@ Indrec
 Cases
 Pretyping
 Unification
+Univdecls
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
new file mode 100644
index 000000000..d7c42d03a
--- /dev/null
+++ b/pretyping/univdecls.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Nameops
+open CErrors
+open Pp
+
+(** Local universes and constraints declarations *)
+type universe_decl =
+  (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let default_univ_decl =
+  let open Misctypes in
+  { univdecl_instance = [];
+    univdecl_extensible_instance = true;
+    univdecl_constraints = Univ.Constraint.empty;
+    univdecl_extensible_constraints = true }
+
+let interp_univ_constraints env evd cstrs =
+  let open Misctypes in
+  let u_of_id x =
+    match x with
+    | Misctypes.GProp -> Loc.tag Univ.Level.prop
+    | GSet  -> Loc.tag Univ.Level.set
+    | GType None | GType (Some (_, Anonymous)) ->
+       user_err ~hdr:"interp_constraint"
+                     (str "Cannot declare constraints on anonymous universes")
+    | GType (Some (loc, Name id)) ->
+       try loc, Evd.universe_of_name evd (Id.to_string id)
+       with Not_found ->
+         user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id)
+  in
+  let interp (evd,cstrs) (u, d, u') =
+    let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in
+    let cstr = (ul,d,u'l) in
+    let cstrs' = Univ.Constraint.add cstr cstrs in
+    try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+        evd, cstrs'
+    with Univ.UniverseInconsistency e ->
+      user_err  ~hdr:"interp_constraint" (str "Universe inconsistency" (* TODO *))
+  in
+  List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl = 
+  let open Misctypes in
+  let pl = decl.univdecl_instance in
+  let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in
+  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+  let decl = { univdecl_instance = pl;
+    univdecl_extensible_instance = decl.univdecl_extensible_instance;
+    univdecl_constraints = cstrs;
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+  in evd, decl
+
+let interp_univ_decl_opt env l =
+  match l with
+  | None -> Evd.from_env env, default_univ_decl
+  | Some decl -> interp_univ_decl env decl
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
new file mode 100644
index 000000000..0c3b749cb
--- /dev/null
+++ b/pretyping/univdecls.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Local universe and constraint declarations. *)
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val default_univ_decl : universe_decl
+
+val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr ->
+                       Evd.evar_map * universe_decl
+
+val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option ->
+                       Evd.evar_map * universe_decl
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5e57f5de0..444a1b2f6 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -37,11 +37,29 @@ open Decl_kinds
     | Some loc -> let (b,_) = Loc.unloc loc in
                   pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id
 
-  let pr_plident (lid, l) =
-    pr_lident lid ++
-    (match l with
-     | Some l -> prlist_with_sep spc pr_lident l
-     | None -> mt())
+  let pr_uconstraint (l, d, r) =
+    pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+      pr_glob_level r
+
+  let pr_univdecl_instance l extensible =
+    prlist_with_sep spc pr_lident l ++
+    (if extensible then str"+" else mt ())
+
+  let pr_univdecl_constraints l extensible =
+    if List.is_empty l && extensible then mt ()
+    else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
+           (if extensible then str"+" else mt())
+
+  let pr_universe_decl l =
+    let open Misctypes in
+    match l with
+    | None -> mt ()
+    | Some l ->
+      str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+        pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+
+  let pr_ident_decl (lid, l) =
+    pr_lident lid ++ pr_universe_decl l
     
   let string_of_fqid fqid =
     String.concat "." (List.map Id.to_string fqid)
@@ -371,24 +389,19 @@ open Decl_kinds
     | l -> spc() ++
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-  let pr_univs pl =
-    match pl with
-    | None -> mt ()
-    | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
-
-  let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
+  let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) =
     let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
     let annot = pr_guard_annot pr_lconstr_expr bl ro in
-    pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
+    pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot
     ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
     ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
     ++ prlist (pr_decl_notation pr_constr) ntn
 
   let pr_statement head (idpl,(bl,c)) =
     assert (not (Option.is_empty idpl));
-    let id, pl = Option.get idpl in
+    let idpl = Option.get idpl in
     hov 2
-      (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
+      (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
          str":" ++ pr_spc_lconstr c)
 
@@ -692,7 +705,7 @@ open Decl_kinds
         return (
           hov 2 (
             pr_def_token d ++ spc()
-            ++ pr_plident id ++ binds ++ typ
+            ++ pr_ident_decl id ++ binds ++ typ
             ++ (match c with
               | None -> mt()
               | Some cc -> str" :=" ++ spc() ++ cc))
@@ -722,7 +735,7 @@ open Decl_kinds
       | VernacAssumption (stre,t,l) ->
         let n = List.length (List.flatten (List.map fst (List.map snd l))) in
         let pr_params (c, (xl, t)) =
-          hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
+          hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
             (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
         let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
         return (hov 2 (pr_assumption_token (n > 1) stre ++
@@ -743,10 +756,10 @@ open Decl_kinds
           | RecordDecl (c,fs) ->
             pr_record_decl b c fs
         in
-        let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
+        let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) =
           hov 0 (
             str key ++ spc() ++
-              (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
+              (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
               pr_and_type_binders_arg indpar ++
               pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
               str" :=") ++ pr_constructor_list k lc ++
@@ -791,8 +804,8 @@ open Decl_kinds
           | Some Local -> keyword "Local" ++ spc ()
           | None | Some Global -> str ""
         in
-        let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
-          pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+        let pr_onecorec ((iddecl,bl,c,def),ntn) =
+          pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
             spc() ++ pr_lconstr_expr c ++
             pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
             prlist (pr_decl_notation pr_constr) ntn
@@ -818,10 +831,6 @@ open Decl_kinds
                    prlist_with_sep (fun _ -> str",") pr_lident v)
         )
       | VernacConstraint v ->
-        let pr_uconstraint (l, d, r) =
-          pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
-            pr_glob_level r
-        in
         return (
           hov 2 (keyword "Constraint" ++ spc () ++
                    prlist_with_sep (fun _ -> str",") pr_uconstraint v)
@@ -875,7 +884,7 @@ open Decl_kinds
             (if abst then keyword "Declare" ++ spc () else mt ()) ++
               keyword "Instance" ++
               (match instid with
-      	 | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () 
+      	 | (loc, Name id), l -> spc () ++ pr_ident_decl ((loc, id),l) ++ spc ()
                | (_, Anonymous), _ -> mt ()) ++
               pr_and_type_binders_arg sup ++
               str":" ++ spc () ++
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 193788558..23f96b5a3 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -239,7 +239,6 @@ let get_current_proof_name = Proof_global.get_current_proof_name
 let get_all_proof_names = Proof_global.get_all_proof_names
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
-type universe_binders = Proof_global.universe_binders
 
 let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
@@ -257,6 +256,5 @@ let set_used_variables l =
 let get_used_variables () =
   Proof_global.get_used_variables ()
 
-let get_universe_binders () =
-  Proof_global.get_universe_binders ()
-
+let get_universe_decl () =
+  Proof_global.get_universe_decl ()
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 745ee8f36..6e4ecd13b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -23,7 +23,7 @@ open Decl_kinds
     proof of mutually dependent theorems) *)
 
 val start_proof :
-  Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -67,6 +67,7 @@ val current_proof_statement :
   unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
+
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
     proof is focused or if there is no [n]th subgoal. [solve SelectAll
@@ -185,8 +186,8 @@ val get_used_variables : unit -> Context.Named.t option
 [@@ocaml.deprecated "use Proof_global.get_used_variables"]
 
 (** {6 Universe binders } *)
-val get_universe_binders : unit -> Proof_global.universe_binders option
-[@@ocaml.deprecated "use Proof_global.get_universe_binders"]
+val get_universe_decl : unit -> Univdecls.universe_decl
+[@@ocaml.deprecated "use Proof_global.get_universe_decl"]
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
@@ -202,7 +203,3 @@ val get_all_proof_names : unit -> Id.t list
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
 [@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]
-
-type universe_binders = Proof_global.universe_binders
-[@@ocaml.deprecated "use Proof_global.universe_binders"]
-
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2ade797f6..e8266f5c8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -69,7 +69,6 @@ let _ =
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
-type universe_binders = Id.t Loc.located list
 
 type proof_object = {
   id : Names.Id.t;
@@ -94,7 +93,7 @@ type pstate = {
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
-  universe_binders: universe_binders option;
+  universe_decl: Univdecls.universe_decl;
 }
 
 let make_terminator f = f
@@ -230,15 +229,22 @@ let activate_proof_mode mode =
 let disactivate_current_proof_mode () =
   CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
-(** [start_proof sigma id str goals terminator] starts a proof of name
+let default_universe_decl =
+  let open Misctypes in
+  { univdecl_instance = [];
+    univdecl_extensible_instance = true;
+    univdecl_constraints = Univ.Constraint.empty;
+    univdecl_extensible_constraints = true }
+
+(** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
-    constraints). *)
-let start_proof sigma id ?pl str goals terminator =
+    constraints), and with universe bindings pl. *)
+let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -247,10 +253,10 @@ let start_proof sigma id ?pl str goals terminator =
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No";
-    universe_binders = pl } in
+    universe_decl = pl } in
   push initial_state pstates
 
-let start_dependent_proof id ?pl str goals terminator =
+let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -259,11 +265,11 @@ let start_dependent_proof id ?pl str goals terminator =
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No";
-    universe_binders = pl } in
+    universe_decl = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
-let get_universe_binders () = (cur_pstate ()).universe_binders
+let get_universe_decl () = (cur_pstate ()).universe_decl
 
 let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
@@ -319,7 +325,7 @@ type closed_proof_output = (Term.constr * Safe_typing.private_constants) list *
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
-  let { pid; section_vars; strength; proof; terminator; universe_binders } =
+  let { pid; section_vars; strength; proof; terminator; universe_decl } =
     cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
@@ -393,8 +399,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
         })
 		fpl initial_goals in
   let binders =
-    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
-	       universe_binders
+    if not poly || (List.is_empty universe_decl.Misctypes.univdecl_instance &&
+                    universe_decl.Misctypes.univdecl_extensible_instance) then None
+    else
+      Some (fst (Evd.check_univ_decl (Evd.from_ctx universes) universe_decl))
   in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 52f5f7404..8c0f6ad85 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -34,7 +34,7 @@ val compact_the_proof : unit -> unit
     values. *)
 type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
-type universe_binders = Names.Id.t Loc.located list
+
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
@@ -54,21 +54,23 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
-(** [start_proof id str goals terminator] starts a proof of name [id]
+(** [start_proof id str pl goals terminator] starts a proof of name [id]
     with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
-    end of the proof to close the proof. *)
+    end of the proof to close the proof. The proof is started in the
+    evar map [sigma] (which can typically contain universe
+    constraints), and with universe bindings pl. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
+  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -119,7 +121,8 @@ val set_used_variables :
   Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
 val get_used_variables : unit -> Context.Named.t option
 
-val get_universe_binders : unit -> universe_binders option
+(** Get the universe declaration associated to the current proof. *)
+val get_universe_decl : unit -> Univdecls.universe_decl
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index ecc988507..0bd8bfe60 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -156,6 +156,38 @@ Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d.
 
 End structures.
 
+
+Module binders.
+
+  Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}.
+    exact A.
+  Defined.
+
+  Definition nomoreu@{i j | i < j} (A : Type@{i}) : Type@{j}.
+    pose(foo:=Type).
+    exact A.
+  Fail Defined.
+  Abort.
+
+  Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}.
+    pose(foo:=Type).
+    exact A.
+  Defined.
+
+  Check moreu@{_ _ _ _}.
+  
+  Fail Definition morec@{i j| } (A : Type@{i}) : Type@{j} := A.
+
+  (* By default constraints are extensible *)
+  Definition morec@{i j} (A : Type@{i}) : Type@{j} := A.
+
+  (* FIXME: not handled in proofs correctly yet *)
+  Lemma bar@{i j | } : Type@{i}.
+    exact Type@{j}.
+  Defined.
+  
+End binders.
+    
 Section cats.
   Local Set Universe Polymorphism.
   Require Import Utf8.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ab1892a18..c21345a2a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -111,14 +111,14 @@ let instance_hook k info global imps ?hook cst =
   Typeclasses.declare_instance (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
+let declare_instance_constant k info global imps ?hook id decl poly evm term termtype =
   let kind = IsDefinition Instance in
   let evm = 
     let levels = Univ.LSet.union (Univops.universes_of_constr termtype) 
 				 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context evm levels 
   in
-  let pl, uctx = Evd.universe_context ?names:pl evm in
+  let pl, uctx = Evd.check_univ_decl evm decl in
   let entry = 
     Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
   in
@@ -129,13 +129,13 @@ let declare_instance_constant k info global imps ?hook id pl poly evm term termt
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
-    ?(generalize=true)
-    ?(tac:unit Proofview.tactic option) ?hook pri =
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
+  poly ctx (instid, bk, cl) props ?(generalize=true)
+  ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let ((loc, instid), pl) = instid in
-  let uctx = Evd.make_evar_universe_context env pl in
-  let evars = ref (Evd.from_ctx uctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evars = ref evd in
   let tclass, ids =
     match bk with
     | Decl_kinds.Implicit ->
@@ -202,7 +202,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	    nf t
 	in
 	Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
-	let pl, ctx = Evd.universe_context ?names:pl !evars in
+	let pl, ctx = Evd.check_univ_decl !evars decl in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
@@ -302,7 +302,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
-	  declare_instance_constant k pri global imps ?hook id pl
+	  declare_instance_constant k pri global imps ?hook id decl
             poly evm (Option.get term) termtype
 	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -323,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
               let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.evar_universe_context evm in
 		ignore (Obligations.add_definition id ?term:constr
- 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+ 			~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
@@ -334,7 +334,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
                      the refinement manually.*)
 		let gls = List.rev (Evd.future_goals evm) in
                 let evm = Evd.reset_future_goals evm in
-                Lemmas.start_proof id ?pl kind evm (EConstr.of_constr termtype)
+                Lemmas.start_proof id ~pl:decl kind evm (EConstr.of_constr termtype)
 		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index fc2fdbbf3..fcdb5c3bc 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -30,7 +30,7 @@ val declare_instance_constant :
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
-  Id.t Loc.located list option ->
+  Univdecls.universe_decl ->
   bool -> (* polymorphic *)
   Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
@@ -43,7 +43,7 @@ val new_instance :
   ?refine:bool -> (** Allow refinement *)
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
-  typeclass_constraint ->
+  Vernacexpr.typeclass_constraint ->
   (bool * constr_expr) option ->
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
diff --git a/vernac/command.ml b/vernac/command.ml
index 32ab5401a..15dacb776 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -91,8 +91,8 @@ let warn_implicits_in_term =
         
 let interp_definition pl bl p red_option c ctypopt =
   let env = Global.env() in
-  let ctx = Evd.make_evar_universe_context env pl in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evdref = ref evd in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
   let nb_args = Context.Rel.nhyps ctx in
@@ -108,7 +108,7 @@ let interp_definition pl bl p red_option c ctypopt =
         let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let vars = Univops.universes_of_constr body in
 	let evd = Evd.restrict_universe_context !evdref vars in
-	let pl, uctx = Evd.universe_context ?names:pl evd in
+	let pl, uctx = Evd.check_univ_decl evd decl in
  	imps1@(Impargs.lift_implicits nb_args imps2), pl,
 	  definition_entry ~univs:uctx ~poly:p body
     | Some ctyp ->
@@ -134,20 +134,20 @@ let interp_definition pl bl p red_option c ctypopt =
         let vars = Univ.LSet.union (Univops.universes_of_constr body) 
           (Univops.universes_of_constr typ) in
         let ctx = Evd.restrict_universe_context !evdref vars in
-	let pl, uctx = Evd.universe_context ?names:pl ctx in
+	let pl, uctx = Evd.check_univ_decl ctx decl in
 	imps1@(Impargs.lift_implicits nb_args impsty), pl,
 	  definition_entry ~types:typ ~poly:p 
 	    ~univs:uctx body
   in
-  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
+  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
 
-let check_definition (ce, evd, _, imps) =
+let check_definition (ce, evd, _, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
-let do_definition ident k pl bl red_option c ctypopt hook =
-  let (ce, evd, pl', imps as def) =
-    interp_definition pl bl (pi2 k) red_option c ctypopt
+let do_definition ident k univdecl bl red_option c ctypopt hook =
+  let (ce, evd, univdecl, pl', imps as def) =
+    interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
     if Flags.is_program_mode () then
       let env = Global.env () in
@@ -164,8 +164,8 @@ let do_definition ident k pl bl red_option c ctypopt hook =
       in
       let ctx = Evd.evar_universe_context evd in
       let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
-	ignore(Obligations.add_definition
-          ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
+      ignore(Obligations.add_definition
+          ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       ignore(DeclareDef.declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
@@ -270,15 +270,15 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
 
 let do_assumptions_bound_univs coe kind nl id pl c =
   let env = Global.env () in
-  let ctx = Evd.make_evar_universe_context env pl in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evdref = ref evd in
   let ty, impls = interp_type_evars_impls env evdref c in
   let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
   let ty = EConstr.Unsafe.to_constr ty in
   let ty = nf ty in
   let vars = Univops.universes_of_constr ty in
   let evd = Evd.restrict_universe_context !evdref vars in
-  let pl, uctx = Evd.universe_context ?names:pl evd in
+  let pl, uctx = Evd.check_univ_decl evd decl in
   let uctx = Univ.ContextSet.of_context uctx in
   let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
   st
@@ -318,7 +318,7 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : lident list option;
+  ind_univs : Vernacexpr.universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -526,8 +526,8 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   List.iter check_param paramsl;
   let env0 = Global.env() in
   let pl = (List.hd indl).ind_univs in
-  let ctx = Evd.make_evar_universe_context env0 pl in
-  let evdref = ref Evd.(from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let evdref = ref evd in
   let impls, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
@@ -576,7 +576,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
   let ctx_params = Context.Rel.map nf ctx_params in
   let evd = !evdref in
-  let pl, uctx = Evd.universe_context ?names:pl evd in
+  let pl, uctx = Evd.check_univ_decl evd decl in
   List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
   Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
@@ -797,7 +797,7 @@ let check_mutuality env evd isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
-  fix_univs : lident list option;
+  fix_univs : universe_decl_expr option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
@@ -917,8 +917,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let ctx = Evd.make_evar_universe_context env pl in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evdref = ref evd in
   let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -1019,6 +1019,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders_rel = nf_evar_context !evdref binders_rel in
   let binders = nf_evar_context !evdref binders in
   let top_arity = Evarutil.nf_evar !evdref top_arity in
+  let pl = Option.map (fun d -> d.univdecl_instance) pl in
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
@@ -1052,7 +1053,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
   let ctx = Evd.evar_universe_context !evdref in
-    ignore(Obligations.add_definition recname ~term:evars_def ?pl
+    ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
 	     evars_typ ctx evars ~hook)
 
 let interp_recursive isfix fixl notations =
@@ -1068,11 +1069,12 @@ let interp_recursive isfix fixl notations =
         | None , acc -> acc
         | x , None -> x
         | Some ls , Some us ->
-	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
+           let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
+	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
 	     user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
 	   Some us) fixl None in
-  let ctx = Evd.make_evar_universe_context env all_universes in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in
+  let evdref = ref evd in
   let fixctxs, fiximppairs, fixannots =
     List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -1122,7 +1124,7 @@ let interp_recursive isfix fixl notations =
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+  (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
   check_evars_are_solved env evd Evd.empty;
@@ -1145,14 +1147,14 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
-      evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1165,8 +1167,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
+    let pl, ctx = Evd.check_univ_decl evd pl in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    let pl, ctx = Evd.universe_context ?names:pl evd in
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
@@ -1179,14 +1181,14 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
       Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1197,8 +1199,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) 
+    let pl, ctx = Evd.check_univ_decl evd pl in
+    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1281,7 +1283,7 @@ let do_program_recursive local p fixkind fixl ntns =
   | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
   | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
   in
-  Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
diff --git a/vernac/command.mli b/vernac/command.mli
index 8d17f27c3..afa97aa24 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -26,11 +26,11 @@ val do_constraint : polymorphic ->
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
+  Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
-      Universes.universe_binders * Impargs.manual_implicits
+                        Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
 
-val do_definition : Id.t -> definition_kind -> lident list option ->
+val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
@@ -49,7 +49,7 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   global_reference * Univ.Instance.t * bool
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
+  Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool
 
 (* val declare_assumptions : variable Loc.located list -> *)
 (*   coercion_flag -> assumption_kind -> types Univ.in_universe_context_set ->  *)
@@ -62,7 +62,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : lident list option;
+  ind_univs : Vernacexpr.universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -102,7 +102,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
-  fix_univs : lident list option;
+  fix_univs : Vernacexpr.universe_decl_expr option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
@@ -127,24 +127,24 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * lident list option * Evd.evar_universe_context * 
+    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * lident list option * Evd.evar_universe_context * 
+    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * lident list option * Evd.evar_universe_context * 
+  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
-  recursive_preentry * lident list option * Evd.evar_universe_context * 
+  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 645320c60..d78cd14f6 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -210,11 +210,11 @@ let compute_proof_name locality = function
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
         user_err ?loc  (pr_id id ++ str " already exists.");
-      id, pl
+      id
   | None ->
-      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
+      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
 
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -222,7 +222,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
+          let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Discharge, VarRef id,imps)
       | Local | Global ->
@@ -232,7 +232,6 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
           | Global -> false
           | Discharge -> assert false
           in
-          let ctx = Univ.ContextSet.to_context ctx in
           let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
           let kn = declare_constant id ~local decl in
           (locality,ConstRef kn,imps))
@@ -250,12 +249,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
       match locality with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
-	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
+	    ~univs:ctx body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
       | Local | Global ->
-        let ctx = Univ.ContextSet.to_context ctx in
         let local = match locality with
         | Local -> true
         | Global -> false
@@ -369,7 +367,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with
+    match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -377,11 +375,11 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with 
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
+    in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization kind ctx recguard thms snl hook =
+let start_proof_with_initialization kind ctx decl recguard thms snl hook =
   let intro_tac (_, (_, (ids, _))) =
     Tacticals.New.tclMAP (function
     | Name id -> Tactics.intro_mustbe_force id
@@ -406,7 +404,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
-  | ((id,pl),(t,(_,imps)))::other_thms ->
+  | (id,(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
         | None -> Evd.empty_evar_universe_context
@@ -418,22 +416,24 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = UState.context_set (*FIXME*) ctx in
+	    let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
 	    let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+            List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
-  let levels = Option.map snd (fst (List.hd thms)) in 
-  let evdref = ref (match levels with
-		    | None -> Evd.from_env env0
-		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
-  in
+  let decl = fst (List.hd thms) in
+  let evd, decl =
+    match decl with
+    | None -> Evd.from_env env0, Univdecls.default_univ_decl
+    | Some decl ->
+       Univdecls.interp_univ_decl_opt env0 (snd decl) in
+  let evdref = ref evd in
   let thms = List.map (fun (sopt,(bl,t)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
@@ -449,16 +449,16 @@ let start_proof_com ?inference_hook kind thms hook =
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
   let () =
-    match levels with
-    | None -> ()
-    | Some l -> ignore (Evd.universe_context evd ?names:l)
+    if not decl.Misctypes.univdecl_extensible_instance then
+       ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance)
+    else ()
   in
   let evd =
     if pi2 kind then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-    start_proof_with_initialization kind evd recguard thms snl hook
+    start_proof_with_initialization kind evd decl recguard thms snl hook
 
 
 (* Saving a proof *)
@@ -507,9 +507,9 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-	    let names = Proof_global.get_universe_binders () in
+	    let decl = Proof_global.get_universe_decl () in
             let evd = Evd.from_ctx universes in
-            let binders, ctx = Evd.universe_context ?names evd in
+            let binders, ctx = Evd.check_univ_decl evd decl in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
 		     (universes, Some binders))
       in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a8c09c0fe..1e23c7314 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -20,13 +20,13 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (EConstr.types -> unit) -> unit
 
-val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
@@ -38,9 +38,9 @@ val start_proof_com :
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_map ->
+  goal_kind -> Evd.evar_map -> Univdecls.universe_decl ->
   (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
-  ((Id.t (* name of thm *) * Proof_global.universe_binders option) *
+  (Id.t (* name of thm *) *
      (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a4fe49020..c71feb52b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -304,7 +304,7 @@ type program_info_aux = {
   prg_body: constr;
   prg_type: constr;
   prg_ctx:  Evd.evar_universe_context;
-  prg_pl: Id.t Loc.located list option;
+  prg_univdecl: Univdecls.universe_decl;
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
@@ -474,8 +474,7 @@ let declare_definition prg =
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Hook.get get_fix_exn () in
-  let pl, ctx =
-    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
+  let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in
   let ce =
     definition_entry ~fix_exn
      ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
@@ -658,7 +657,7 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
   let obls', b =
     match b with
@@ -679,7 +678,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 	  obls, b
   in
     { prg_name = n ; prg_body = b; prg_type = reduce t; 
-      prg_ctx = ctx; prg_pl = pl;
+      prg_ctx = ctx; prg_univdecl = udecl;
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
@@ -1068,11 +1067,12 @@ let show_term n =
 	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
-let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
+                   ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Decls.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1087,13 +1087,14 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic
+                           ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Decls.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 5614403ba..11c2553ae 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -53,7 +53,7 @@ val default_tactic : unit Proofview.tactic ref
 
 val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   Evd.evar_universe_context ->
-  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
+  ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
@@ -71,7 +71,7 @@ val add_mutual_definitions :
   (Names.Id.t * Term.constr * Term.types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   Evd.evar_universe_context ->
-  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
+  ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
diff --git a/vernac/record.ml b/vernac/record.ml
index a2e443e5f..4fb607dec 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -95,8 +95,8 @@ let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields finite def id pl t ps nots fs =
   let env0 = Global.env () in
-  let ctx = Evd.make_evar_universe_context env0 pl in
-  let evars = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let evars = ref evd in
   let _ = 
     let error bk (loc, name) = 
       match bk, name with
@@ -165,9 +165,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
   let newps = List.map (EConstr.to_rel_decl evars) newps in
   let typ = EConstr.to_constr evars typ in
   let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
+  let univs = Evd.check_univ_decl evars decl in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
-    Evd.universe_context ?names:pl evars, typ, template, imps, newps, impls, newfs
+    univs, typ, template, imps, newps, impls, newfs
 
 let degenerate_decl decl =
   let id = match RelDecl.get_name decl with
diff --git a/vernac/record.mli b/vernac/record.mli
index 9a0c9ef9d..aea474581 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -39,7 +39,7 @@ val declare_structure :
 
 val definition_structure :
   inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
-  Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list *
+  Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference