Allow declaring universe constraints at definition level.

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

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

10 files changed, 105 insertions, 101 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ab1892a18e..c21345a2aa 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 fc2fdbbf34..fcdb5c3bc5 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 32ab5401a0..15dacb7760 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -91,8 +91,8 @@ let warn_implicits_in_term =
         
 let interp_definition pl bl p red_option c ctypopt =
   let env = Global.env() in
-  let ctx = Evd.make_evar_universe_context env pl in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evdref = ref evd in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
   let nb_args = Context.Rel.nhyps ctx in
@@ -108,7 +108,7 @@ let interp_definition pl bl p red_option c ctypopt =
         let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let vars = Univops.universes_of_constr body in
 	let evd = Evd.restrict_universe_context !evdref vars in
-	let pl, uctx = Evd.universe_context ?names:pl evd in
+	let pl, uctx = Evd.check_univ_decl evd decl in
  	imps1@(Impargs.lift_implicits nb_args imps2), pl,
 	  definition_entry ~univs:uctx ~poly:p body
     | Some ctyp ->
@@ -134,20 +134,20 @@ let interp_definition pl bl p red_option c ctypopt =
         let vars = Univ.LSet.union (Univops.universes_of_constr body) 
           (Univops.universes_of_constr typ) in
         let ctx = Evd.restrict_universe_context !evdref vars in
-	let pl, uctx = Evd.universe_context ?names:pl ctx in
+	let pl, uctx = Evd.check_univ_decl ctx decl in
 	imps1@(Impargs.lift_implicits nb_args impsty), pl,
 	  definition_entry ~types:typ ~poly:p 
 	    ~univs:uctx body
   in
-  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
+  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
 
-let check_definition (ce, evd, _, imps) =
+let check_definition (ce, evd, _, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
-let do_definition ident k pl bl red_option c ctypopt hook =
-  let (ce, evd, pl', imps as def) =
-    interp_definition pl bl (pi2 k) red_option c ctypopt
+let do_definition ident k univdecl bl red_option c ctypopt hook =
+  let (ce, evd, univdecl, pl', imps as def) =
+    interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
     if Flags.is_program_mode () then
       let env = Global.env () in
@@ -164,8 +164,8 @@ let do_definition ident k pl bl red_option c ctypopt hook =
       in
       let ctx = Evd.evar_universe_context evd in
       let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
-	ignore(Obligations.add_definition
-          ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
+      ignore(Obligations.add_definition
+          ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       ignore(DeclareDef.declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
@@ -270,15 +270,15 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
 
 let do_assumptions_bound_univs coe kind nl id pl c =
   let env = Global.env () in
-  let ctx = Evd.make_evar_universe_context env pl in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evdref = ref evd in
   let ty, impls = interp_type_evars_impls env evdref c in
   let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
   let ty = EConstr.Unsafe.to_constr ty in
   let ty = nf ty in
   let vars = Univops.universes_of_constr ty in
   let evd = Evd.restrict_universe_context !evdref vars in
-  let pl, uctx = Evd.universe_context ?names:pl evd in
+  let pl, uctx = Evd.check_univ_decl evd decl in
   let uctx = Univ.ContextSet.of_context uctx in
   let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
   st
@@ -318,7 +318,7 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : lident list option;
+  ind_univs : Vernacexpr.universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -526,8 +526,8 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   List.iter check_param paramsl;
   let env0 = Global.env() in
   let pl = (List.hd indl).ind_univs in
-  let ctx = Evd.make_evar_universe_context env0 pl in
-  let evdref = ref Evd.(from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let evdref = ref evd in
   let impls, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
@@ -576,7 +576,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
   let ctx_params = Context.Rel.map nf ctx_params in
   let evd = !evdref in
-  let pl, uctx = Evd.universe_context ?names:pl evd in
+  let pl, uctx = Evd.check_univ_decl evd decl in
   List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
   Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
@@ -797,7 +797,7 @@ let check_mutuality env evd isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
-  fix_univs : lident list option;
+  fix_univs : universe_decl_expr option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
@@ -917,8 +917,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let ctx = Evd.make_evar_universe_context env pl in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evdref = ref evd in
   let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -1019,6 +1019,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders_rel = nf_evar_context !evdref binders_rel in
   let binders = nf_evar_context !evdref binders in
   let top_arity = Evarutil.nf_evar !evdref top_arity in
+  let pl = Option.map (fun d -> d.univdecl_instance) pl in
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
@@ -1052,7 +1053,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
   let ctx = Evd.evar_universe_context !evdref in
-    ignore(Obligations.add_definition recname ~term:evars_def ?pl
+    ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
 	     evars_typ ctx evars ~hook)
 
 let interp_recursive isfix fixl notations =
@@ -1068,11 +1069,12 @@ let interp_recursive isfix fixl notations =
         | None , acc -> acc
         | x , None -> x
         | Some ls , Some us ->
-	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
+           let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
+	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
 	     user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
 	   Some us) fixl None in
-  let ctx = Evd.make_evar_universe_context env all_universes in
-  let evdref = ref (Evd.from_ctx ctx) in
+  let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in
+  let evdref = ref evd in
   let fixctxs, fiximppairs, fixannots =
     List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -1122,7 +1124,7 @@ let interp_recursive isfix fixl notations =
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+  (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
   check_evars_are_solved env evd Evd.empty;
@@ -1145,14 +1147,14 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
-      evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1165,8 +1167,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
+    let pl, ctx = Evd.check_univ_decl evd pl in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    let pl, ctx = Evd.universe_context ?names:pl evd in
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
@@ -1179,14 +1181,14 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
       Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1197,8 +1199,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) 
+    let pl, ctx = Evd.check_univ_decl evd pl in
+    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1281,7 +1283,7 @@ let do_program_recursive local p fixkind fixl ntns =
   | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
   | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
   in
-  Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
diff --git a/vernac/command.mli b/vernac/command.mli
index 8d17f27c30..afa97aa24f 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -26,11 +26,11 @@ val do_constraint : polymorphic ->
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
+  Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
-      Universes.universe_binders * Impargs.manual_implicits
+                        Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
 
-val do_definition : Id.t -> definition_kind -> lident list option ->
+val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
@@ -49,7 +49,7 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   global_reference * Univ.Instance.t * bool
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
+  Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool
 
 (* val declare_assumptions : variable Loc.located list -> *)
 (*   coercion_flag -> assumption_kind -> types Univ.in_universe_context_set ->  *)
@@ -62,7 +62,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : lident list option;
+  ind_univs : Vernacexpr.universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -102,7 +102,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
-  fix_univs : lident list option;
+  fix_univs : Vernacexpr.universe_decl_expr option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
@@ -127,24 +127,24 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * lident list option * Evd.evar_universe_context * 
+    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * lident list option * Evd.evar_universe_context * 
+    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * lident list option * Evd.evar_universe_context * 
+  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
-  recursive_preentry * lident list option * Evd.evar_universe_context * 
+  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 645320c603..d78cd14f69 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -210,11 +210,11 @@ let compute_proof_name locality = function
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
         user_err ?loc  (pr_id id ++ str " already exists.");
-      id, pl
+      id
   | None ->
-      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
+      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
 
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -222,7 +222,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
+          let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Discharge, VarRef id,imps)
       | Local | Global ->
@@ -232,7 +232,6 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
           | Global -> false
           | Discharge -> assert false
           in
-          let ctx = Univ.ContextSet.to_context ctx in
           let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
           let kn = declare_constant id ~local decl in
           (locality,ConstRef kn,imps))
@@ -250,12 +249,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
       match locality with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
-	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
+	    ~univs:ctx body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
       | Local | Global ->
-        let ctx = Univ.ContextSet.to_context ctx in
         let local = match locality with
         | Local -> true
         | Global -> false
@@ -369,7 +367,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with
+    match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -377,11 +375,11 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with 
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
+    in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization kind ctx recguard thms snl hook =
+let start_proof_with_initialization kind ctx decl recguard thms snl hook =
   let intro_tac (_, (_, (ids, _))) =
     Tacticals.New.tclMAP (function
     | Name id -> Tactics.intro_mustbe_force id
@@ -406,7 +404,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
-  | ((id,pl),(t,(_,imps)))::other_thms ->
+  | (id,(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
         | None -> Evd.empty_evar_universe_context
@@ -418,22 +416,24 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = UState.context_set (*FIXME*) ctx in
+	    let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
 	    let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+            List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
-  let levels = Option.map snd (fst (List.hd thms)) in 
-  let evdref = ref (match levels with
-		    | None -> Evd.from_env env0
-		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
-  in
+  let decl = fst (List.hd thms) in
+  let evd, decl =
+    match decl with
+    | None -> Evd.from_env env0, Univdecls.default_univ_decl
+    | Some decl ->
+       Univdecls.interp_univ_decl_opt env0 (snd decl) in
+  let evdref = ref evd in
   let thms = List.map (fun (sopt,(bl,t)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
@@ -449,16 +449,16 @@ let start_proof_com ?inference_hook kind thms hook =
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
   let () =
-    match levels with
-    | None -> ()
-    | Some l -> ignore (Evd.universe_context evd ?names:l)
+    if not decl.Misctypes.univdecl_extensible_instance then
+       ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance)
+    else ()
   in
   let evd =
     if pi2 kind then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-    start_proof_with_initialization kind evd recguard thms snl hook
+    start_proof_with_initialization kind evd decl recguard thms snl hook
 
 
 (* Saving a proof *)
@@ -507,9 +507,9 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-	    let names = Proof_global.get_universe_binders () in
+	    let decl = Proof_global.get_universe_decl () in
             let evd = Evd.from_ctx universes in
-            let binders, ctx = Evd.universe_context ?names evd in
+            let binders, ctx = Evd.check_univ_decl evd decl in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
 		     (universes, Some binders))
       in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a8c09c0fed..1e23c7314b 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 a4fe49020a..c71feb52b3 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -304,7 +304,7 @@ type program_info_aux = {
   prg_body: constr;
   prg_type: constr;
   prg_ctx:  Evd.evar_universe_context;
-  prg_pl: Id.t Loc.located list option;
+  prg_univdecl: Univdecls.universe_decl;
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
@@ -474,8 +474,7 @@ let declare_definition prg =
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Hook.get get_fix_exn () in
-  let pl, ctx =
-    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
+  let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in
   let ce =
     definition_entry ~fix_exn
      ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
@@ -658,7 +657,7 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
   let obls', b =
     match b with
@@ -679,7 +678,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 	  obls, b
   in
     { prg_name = n ; prg_body = b; prg_type = reduce t; 
-      prg_ctx = ctx; prg_pl = pl;
+      prg_ctx = ctx; prg_univdecl = udecl;
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
@@ -1068,11 +1067,12 @@ let show_term n =
 	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
-let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
+                   ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Decls.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1087,13 +1087,14 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic
+                           ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Decls.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 5614403ba5..11c2553ae1 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 a2e443e5f7..4fb607deca 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 9a0c9ef9d1..aea474581e 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