Merge PR #688: Binding universe constraints in Definition/Inductive/etc...

46 files changed, 588 insertions, 311 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 50fbee529..654d93485 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
@@ -2300,7 +2308,7 @@ sig
     val universe_context_set : evar_map -> Univ.ContextSet.t
     val evar_ident : evar -> evar_map -> Names.Id.t option
     val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-    val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map ->
+    val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
                            (Names.Id.t * Univ.Level.t) list * Univ.UContext.t
     val nf_constraints : evar_map -> evar_map
     val from_ctx : UState.t -> evar_map
@@ -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
 
@@ -3704,6 +3711,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
@@ -3721,9 +3732,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
@@ -3737,18 +3746,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
 
@@ -3826,12 +3837,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
@@ -3855,7 +3866,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
@@ -3946,7 +3957,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 *)
@@ -4083,6 +4094,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/                                       *)
 (************************************************************************)
@@ -4481,12 +4504,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
@@ -5540,7 +5562,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 ->
@@ -5616,7 +5638,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;
@@ -5625,7 +5647,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
   }
@@ -5641,7 +5663,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
 
@@ -5654,7 +5676,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 :
@@ -5682,7 +5704,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..f1b5419de 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -748,7 +748,10 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let universe_context ?names evd = UState.universe_context ?names evd.universes
+let universe_context ~names ~extensible evd =
+  UState.universe_context ~names ~extensible evd.universes
+
+let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
 
 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..abcabe815 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context
 val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
-val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context
 
 
 val evar_universe_context_of_binders :
@@ -547,11 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : ?names:(Id.t located) list -> evar_map ->
+val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
 		       (Id.t * Univ.Level.t) list * Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
+val check_univ_decl : evar_map -> UState.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..13a9bb373 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -97,17 +97,9 @@ let subst ctx = ctx.uctx_univ_variables
 
 let ugraph ctx = ctx.uctx_universes
 
-let algebraics ctx = ctx.uctx_univ_algebraic
+let initial_graph ctx = ctx.uctx_initial_universes
 
-let constrain_variables diff ctx =
-  Univ.LSet.fold
-    (fun l cstrs ->
-      try
-        match Univ.LMap.find l ctx.uctx_univ_variables with
-        | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
-        | None -> cstrs
-      with Not_found | Option.IsNone -> cstrs)
-    diff Univ.Constraint.empty
+let algebraics ctx = ctx.uctx_univ_algebraic
 
 let add_uctx_names ?loc s l (names, names_rev) =
   (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
@@ -240,6 +232,24 @@ let add_universe_constraints ctx cstrs =
       uctx_univ_variables = vars;
       uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
+let constrain_variables diff ctx =
+  let univs, local = ctx.uctx_local in
+  let univs, vars, local =
+    Univ.LSet.fold
+      (fun l (univs, vars, cstrs) ->
+        try
+          match Univ.LMap.find l vars with
+          | Some u ->
+             (Univ.LSet.add l univs,
+              Univ.LMap.remove l vars,
+              Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs)
+          | None -> (univs, vars, cstrs)
+        with Not_found | Option.IsNone -> (univs, vars, cstrs))
+      diff (univs, ctx.uctx_univ_variables, local)
+  in
+  { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
+  
+
 let pr_uctx_level uctx = 
   let map, map_rev = uctx.uctx_names in 
     fun l ->
@@ -247,41 +257,63 @@ let pr_uctx_level uctx =
       with Not_found | Option.IsNone ->
         Universes.pr_with_global_universes l
 
-let universe_context ?names ctx =
-  match names with
-  | None -> [], Univ.ContextSet.to_context ctx.uctx_local
-  | Some pl ->
-     let levels = Univ.ContextSet.levels ctx.uctx_local in
-     let newinst, map, left =
-       List.fold_right
-         (fun (loc,id) (newinst, map, acc) ->
-          let l =
-            try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
-            with Not_found ->
-              user_err ?loc ~hdr:"universe_context"
-                            (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
-          in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
-         pl ([], [], levels)
-     in
-       if not (Univ.LSet.is_empty left) then
-         let n = Univ.LSet.cardinal left in
-         let loc =
-           try
-             let info =
-               Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
-             info.uloc
-           with Not_found -> None
-         in
-           user_err ?loc ~hdr:"universe_context"
-                        ((str(CString.plural n "Universe") ++ spc () ++
-			     Univ.LSet.pr (pr_uctx_level ctx) left ++
-			   spc () ++ str (CString.conjugate_verb_to_be n) ++
-                           str" unbound."))
-      else
-        let inst = Univ.Instance.of_array (Array.of_list newinst) in
-        let ctx = Univ.UContext.make (inst,
-          Univ.ContextSet.constraints ctx.uctx_local)
-        in map, ctx
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let universe_context ~names ~extensible ctx =
+  let levels = Univ.ContextSet.levels ctx.uctx_local in
+  let newinst, left =
+    List.fold_right
+      (fun (loc,id) (newinst, acc) ->
+         let l =
+           try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+           with Not_found ->
+             user_err ?loc ~hdr:"universe_context"
+               (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+         in (l :: newinst, Univ.LSet.remove l acc))
+      names ([], levels)
+  in
+  if not extensible && not (Univ.LSet.is_empty left) then
+    let n = Univ.LSet.cardinal left in
+    let loc =
+      try
+        let info =
+          Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+        info.uloc
+      with Not_found -> None
+    in
+    user_err ?loc ~hdr:"universe_context"
+      ((str(CString.plural n "Universe") ++ spc () ++
+	Univ.LSet.pr (pr_uctx_level ctx) left ++
+	spc () ++ str (CString.conjugate_verb_to_be n) ++
+        str" unbound."))
+  else
+    let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
+    let inst = Array.append (Array.of_list newinst) left in
+    let inst = Univ.Instance.of_array inst in
+    let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in
+    let ctx = Univ.UContext.make (inst,
+                                  Univ.ContextSet.constraints ctx.uctx_local) in
+    map, ctx
+
+let check_implication uctx cstrs ctx =
+  let gr = 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 uctx decl =
+  let open Misctypes in
+  let pl, ctx = universe_context
+      ~names:decl.univdecl_instance
+      ~extensible:decl.univdecl_extensible_instance
+      uctx
+  in
+  if not decl.univdecl_extensible_constraints then
+    check_implication uctx decl.univdecl_constraints ctx;
+  pl, ctx
 
 let restrict ctx vars =
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
diff --git a/engine/uState.mli b/engine/uState.mli
index d198fbfbe..c44f2c1d7 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. *)
@@ -105,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
 
 val normalize_variables : t -> Univ.universe_subst * t
 
-val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> t -> t
 
 val abstract_undefined_variables : t -> t
 
@@ -115,9 +118,26 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 val normalize : t -> t
 
-(** {5 TODO: Document me} *)
+(** [universe_context names extensible ctx]
+
+    Return a universe context containing the local universes of [ctx]
+    and their constraints. The universes corresponding to [names] come
+    first in the order defined by that list.
+
+    If [extensible] is false, check that the universes of [names] are
+    the only local universes.
 
-val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+    Also return the association list of universe names and universes
+    (including those not in [names]). *)
+val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
+  (Id.t * Univ.Level.t) list * Univ.universe_context
+
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
+
+(** {5 TODO: Document me} *)
 
 val update_sigma_env : t -> Environ.env -> t
 
diff --git a/engine/universes.ml b/engine/universes.ml
index 686411e7d..7f5bf24b7 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 fb713d352..cfc3343b6 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
@@ -333,12 +340,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
@@ -347,7 +354,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/kernel/univ.mli b/kernel/univ.mli
index a4f2e26b6..94116e473 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -411,6 +411,7 @@ sig
   val add_instance : Instance.t -> t -> t
 
   (** Arbitrary choice of linear order of the variables *)
+  val sort_levels : Level.t array -> Level.t array
   val to_context : t -> universe_context
   val of_context : universe_context -> t
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7d0728458..4e8b98fcf 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -301,7 +301,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   instance:
-    [ [ "@{"; l = LIST1 universe_level; "}" -> Some l
+    [ [ "@{"; l = LIST0 universe_level; "}" -> Some l
       | -> None ] ]
   ;
   universe_level:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0da22fd71..4a59b8597 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -138,13 +138,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 ->
@@ -152,7 +152,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)
@@ -224,13 +224,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)
+              | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ]
+         ->
+         { 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)
@@ -288,7 +304,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) ] ]
@@ -314,14 +330,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) ] ]
   ;
@@ -393,7 +409,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)) ] ]
   ;
 
@@ -796,7 +812,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/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ef1654fdf..409bb89ee 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -338,13 +338,14 @@ let generate_functional_principle (evd: Evd.evar_map ref)
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
-	let evd' = Evd.from_env (Global.env ()) in
-	let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
-	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
-	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
-	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
+        let evd' = Evd.from_env (Global.env ()) in
+        let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
+        let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+        let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+        let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
+        (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+        let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in
+        let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
 	ignore(
 	  Declare.declare_constant
 	    name
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 41a10cba3..d43fd78f3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1543,7 +1543,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
+  let functional_ref =
+    let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in
+    declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
+  in
   (* Refresh the global universes, now including those of _F *)
   let evm = Evd.from_env (Global.env ()) in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75b665aad..3d01cbe8d 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,7 +1884,7 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let pl, ctx = Evd.universe_context sigma in
+  let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
   let typ = EConstr.to_constr sigma typ in
   let term = EConstr.to_constr sigma term in
   let cst = 
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/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d0fe1f957..b8fae2494 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
   let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
   let nf c = nf (constr_of c) in
-  Array.map nf !tactic_res, snd (Evd.universe_context evd)
+  Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd)
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
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 51c3eb212..f371fb08c 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)
 
@@ -686,7 +699,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))
@@ -716,7 +729,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 ++
@@ -737,10 +750,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 ++
@@ -785,8 +798,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
@@ -812,10 +825,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)
@@ -869,7 +878,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..cd4d1dcf6 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
@@ -312,20 +318,21 @@ let get_open_goals () =
 
 let constrain_variables init uctx =
   let levels = Univ.Instance.levels (Univ.UContext.instance init) in
-  let cstrs = UState.constrain_variables levels uctx in
-  Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
+  UState.constrain_variables levels uctx
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 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
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
+  let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
+  let binders = if poly then Some binders else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -349,53 +356,54 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = constrain_variables initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
-           * complement the univ constraints of the typ with the ones of
-           * the body.  So we keep the two sets distinct. *)
+             complement the univ constraints of the typ with the ones of
+             the body.  So we keep the two sets distinct. *)
 	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = Univops.restrict_universe_context ctx used_univs in
-          (initunivs, typ), ((body, ctx_body), eff)
+          let ctx_body = UState.restrict ctx used_univs in
+          let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
+          (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
         else
-          let initunivs = Univ.UContext.empty in
-          let ctx = constrain_variables initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
-           * constraints in which we merge the ones for the body and the ones
-           * for the typ *)
+             constraints in which we merge the ones for the body and the ones
+             for the typ. We recheck the declaration after restricting with
+             the actually used universes.
+             TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = Univops.restrict_universe_context ctx used_univs in
-          let univs = Univ.ContextSet.to_context ctx in
+          let ctx = UState.restrict universes used_univs in
+          let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
     else
       fun t p ->
-        let initunivs = Evd.evar_context_universe_context initial_euctx in
-        Future.from_val (initunivs, nf t),
+        Future.from_val (univctx, nf t),
         Future.chain ~pure:true p (fun (pt,eff) ->
-          (pt,constrain_variables initunivs (Future.force univs)),eff)
+          (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+          let bodyunivs = constrain_variables univctx (Future.force univs) in
+          let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
+          (pt,Univ.ContextSet.of_context univs),eff)
   in
-  let entries =
-    Future.map2 (fun p (_, t) ->
-      let t = EConstr.Unsafe.to_constr t in
-      let univstyp, body = make_body t p in
-      let univs, typ = Future.force univstyp in
-      let univs =
-        if poly then Entries.Polymorphic_const_entry univs
-        else Entries.Monomorphic_const_entry univs
-      in
-	{ Entries.
-	  const_entry_body = body;
-	  const_entry_secctx = section_vars;
-	  const_entry_feedback = feedback_id;
-	  const_entry_type  = Some typ;
-	  const_entry_inline_code = false;
-	  const_entry_opaque = true;
-	  const_entry_universes = univs;
-        })
-		fpl initial_goals in
-  let binders =
-    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
-	       universe_binders
+  let entry_fn p (_, t) =
+    let t = EConstr.Unsafe.to_constr t in
+    let univstyp, body = make_body t p in
+    let univs, typ = Future.force univstyp in
+    let univs =
+      if poly then Entries.Polymorphic_const_entry univs
+      else Entries.Monomorphic_const_entry univs
+    in
+    {Entries.
+      const_entry_body = body;
+      const_entry_secctx = section_vars;
+      const_entry_feedback = feedback_id;
+      const_entry_type  = Some typ;
+      const_entry_inline_code = false;
+      const_entry_opaque = true;
+      const_entry_universes = univs; }
   in
+  let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
   fun pr_ending -> CEphemeron.get terminator pr_ending
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/tactics/leminv.ml b/tactics/leminv.ml
index 967ec2a71..7c488f524 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
   let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
-    p, Evd.universe_context sigma
+    p, Evd.universe_context ~names:[] ~extensible:true sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 128bc7767..904ff68aa 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -4,3 +4,9 @@ bar@{u} = nat
          *)
 
 bar is universe polymorphic
+foo@{u Top.8 v} = 
+Type@{Top.8} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1, Top.8+1, v+1)}
+(* u Top.8 v |=  *)
+
+foo is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index d9e89e43c..8656ff1a3 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,7 +1,13 @@
 Set Universe Polymorphism.
 Set Printing Universes.
+Unset Strict Universe Declaration.
 
 Class Wrap A := wrap : A.
 
 Instance bar@{u} : Wrap@{u} Set. Proof nat.
 Print bar.
+
+(* The universes in the binder come first, then the extra universes in
+   order of appearance. *)
+Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
+Print foo.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index ecc988507..7eaafc354 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -156,6 +156,52 @@ Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d.
 
 End structures.
 
+
+Module binders.
+
+  Definition mynat@{|} := nat.
+
+  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 *)
+  Polymorphic Definition morec@{i j} (A : Type@{i}) : Type@{j} := A.
+  Check morec@{_ _}.
+
+  (* Handled in proofs as well *)
+  Lemma bar@{i j | } : Type@{i}.
+    exact Type@{j}.
+    Fail Defined.
+  Abort.
+
+  Lemma bar@{i j| i < j} : Type@{j}.
+  Proof.
+    exact Type@{i}.
+  Qed.
+
+  Lemma barext@{i j|+} : Type@{j}.
+  Proof.
+    exact Type@{i}.
+  Qed.
+
+End binders.
+    
 Section cats.
   Local Set Universe Polymorphism.
   Require Import Utf8.
diff --git a/vernac/class.ml b/vernac/class.ml
index be682977e..3915148a0 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -222,9 +222,10 @@ let build_id_coercion idf_opt source poly =
 	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
+  let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma))
+      (definition_entry ~types:typ_f ~poly ~univs
 	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
   in
   let decl = (constr_entry, IsDefinition IdentityCoercion) in
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 b611edc41..120f9590f 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -90,8 +90,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
@@ -107,7 +107,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 ->
@@ -133,20 +133,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
@@ -163,8 +163,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
@@ -269,15 +269,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
@@ -317,7 +317,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
 }
@@ -525,8 +525,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
@@ -575,7 +575,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,_) ->
@@ -796,7 +796,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;
@@ -916,8 +916,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
@@ -1018,14 +1018,16 @@ 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 hook, recname, typ = 
+  let pl, plext = Option.cata
+      (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
+  let hook, recname, typ =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
       let hook l gr _ = 
 	let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let ty = EConstr.Unsafe.to_constr ty in
-	let pl, univs = Evd.universe_context ?names:pl !evdref in
+	let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
 	  (*FIXME poly? *)
 	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
 	(** FIXME: include locality *)
@@ -1051,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 =
@@ -1067,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
@@ -1121,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;
@@ -1144,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
@@ -1164,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 *)
@@ -1178,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
@@ -1196,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
@@ -1280,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/indschemes.ml b/vernac/indschemes.ml
index facebd096..90168843a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -108,7 +108,7 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
-  let _, univs = Evd.universe_context ctx in
+  let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in
   let univs =
     if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
     else Monomorphic_const_entry univs
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 590fa6213..4b36c2d07 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -48,7 +48,7 @@ let retrieve_first_recthm uctx = function
       (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      let (_, uctx) = UState.universe_context uctx in
+      let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in
       let inst = Univ.UContext.instance uctx in
       let map (c, ctx) = Vars.subst_instance_constr inst c in
       (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -209,11 +209,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 ->
@@ -221,7 +221,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 ->
@@ -231,7 +231,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))
@@ -249,12 +248,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
@@ -368,7 +366,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
@@ -376,11 +374,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
@@ -405,7 +403,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
@@ -417,22 +415,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
@@ -448,16 +448,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 ~extensible:false)
+    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 *)
@@ -506,11 +506,13 @@ 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
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
-		     (universes, Some binders))
+            let binders, ctx = Evd.check_univ_decl evd decl in
+            let poly = pi2 k in
+            let binders = if poly then Some binders else None in
+            Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
+		     (universes, binders))
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
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..89b18d254 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; 
@@ -889,7 +888,7 @@ in
       let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
       Univ.Instance.empty, Evd.evar_universe_context ctx'
     else
-      let (_, uctx) = UState.universe_context ctx' in
+      let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in
       Univ.UContext.instance uctx, ctx'
   in
   let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
@@ -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
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c7b8def0e..ee84ff101 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1555,7 +1555,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
   let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
-  let pl, uctx = Evd.universe_context sigma' in
+  let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in
   let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =