Separate checking univ_decls and obtaining universe binder names.

8 files changed, 51 insertions, 47 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index 44f20a088..e59482b71 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -212,7 +212,7 @@ 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 univs = 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
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ed37bab6d..6f5f96ee2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
 				 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context evm levels 
   in
-  let pl, uctx = Evd.check_univ_decl evm decl in
+  let uctx = Evd.check_univ_decl evm decl in
   let entry = 
     Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
-    Universes.register_universe_binders (ConstRef kn) pl;
+    Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
@@ -203,12 +203,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	    nf t
 	in
 	Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
-	let pl, ctx = Evd.check_univ_decl !evars decl in
+        let 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)
 	in
-	  Universes.register_universe_binders (ConstRef cst) pl;
+          Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
 	  instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
diff --git a/vernac/command.ml b/vernac/command.ml
index 5d83de070..5a063f173 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -107,8 +107,9 @@ 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.check_univ_decl evd decl in
- 	imps1@(Impargs.lift_implicits nb_args imps2), pl,
+        let uctx = Evd.check_univ_decl evd decl in
+        let binders = Evd.universe_binders evd in
+        imps1@(Impargs.lift_implicits nb_args imps2), binders,
 	  definition_entry ~univs:uctx ~poly:p body
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -133,8 +134,9 @@ 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.check_univ_decl ctx decl in
-	imps1@(Impargs.lift_implicits nb_args impsty), pl,
+        let uctx = Evd.check_univ_decl ctx decl in
+        let binders = Evd.universe_binders evd in
+        imps1@(Impargs.lift_implicits nb_args impsty), binders,
 	  definition_entry ~types:typ ~poly:p 
 	    ~univs:uctx body
   in
@@ -277,9 +279,10 @@ let do_assumptions_bound_univs coe kind nl id pl c =
   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.check_univ_decl evd decl in
+  let uctx = Evd.check_univ_decl evd decl in
+  let binders = Evd.universe_binders evd in
   let uctx = Univ.ContextSet.of_context uctx in
-  let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
+  let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in
   st
 
 let do_assumptions kind nl l = match l with
@@ -576,7 +579,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.check_univ_decl evd decl in
+  let 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,_) ->
@@ -617,7 +620,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   in
   (if poly && cum then
       Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
-   else mind_ent), pl, impls
+   else mind_ent), Evd.universe_binders evd, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -1025,17 +1028,18 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     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 ~extensible:plext !evdref in
-	  (*FIXME poly? *)
-	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
-	(** FIXME: include locality *)
-	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
-	let gr = ConstRef c in
-	  if Impargs.is_implicit_args () || not (List.is_empty impls) then
-	    Impargs.declare_manual_implicits false gr [impls]
+        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 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 *)
+        let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+        let gr = ConstRef c in
+        let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in
+        if Impargs.is_implicit_args () || not (List.is_empty impls) then
+          Impargs.declare_manual_implicits false gr [impls]
       in
       let typ = it_mkProd_or_LetIn top_arity binders in
 	hook, name, typ
@@ -1168,7 +1172,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 ctx = Evd.check_univ_decl evd pl in
+    let pl = Evd.universe_binders evd in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
@@ -1200,7 +1205,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.check_univ_decl evd pl in
+    let ctx = Evd.check_univ_decl evd pl in
+    let pl = Evd.universe_binders evd in
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c0ddc7e2c..58f39e303 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,7 +109,7 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
-  let _, univs = Evd.universe_context ~names:[] ~extensible:true 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 a025bfff8..cd30c7a68 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,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 ~names:[] ~extensible:true 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)
@@ -223,7 +223,7 @@ let compute_proof_name locality = function
     let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
       next_global_ident_away default_thm_id avoid
 
-let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -420,9 +420,9 @@ let start_proof_with_initialization kind ctx decl 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 binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
+            let 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 binders body opaq) 1 other_thms in
+            List.map_i (save_remaining_recthms kind norm ctx 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;
@@ -513,9 +513,9 @@ let save_proof ?proof = function
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
             let evd = Evd.from_ctx universes in
-            let binders, ctx = Evd.check_univ_decl evd decl in
+            let ctx = Evd.check_univ_decl evd decl in
             let poly = pi2 k in
-            let binders = if poly then Some binders else None in
+            let binders = if poly then Some (UState.universe_binders universes) else None in
             Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
 		     (universes, binders))
       in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 590332d08..216801811 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -475,20 +475,17 @@ 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.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in
+  let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in
   let ce =
     definition_entry ~fix_exn
      ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
   let () = progmap_remove prg in
-  let cst =
-    DeclareDef.declare_definition prg.prg_name
-     prg.prg_kind ce Universes.empty_binders prg.prg_implicits
-     (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
-  in
-  Universes.register_universe_binders cst pl;
-  cst
+  let ubinders = UState.universe_binders prg.prg_ctx in
+  DeclareDef.declare_definition prg.prg_name
+    prg.prg_kind ce ubinders prg.prg_implicits
+    (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -893,7 +890,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 ~names:[] ~extensible:true 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
diff --git a/vernac/record.ml b/vernac/record.ml
index 6ffbd1584..9fef8f682 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -168,9 +168,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
   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
+  let ubinders = Evd.universe_binders evars in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
-    univs, typ, template, imps, newps, impls, newfs
+    ubinders, univs, typ, template, imps, newps, impls, newfs
 
 let degenerate_decl decl =
   let id = match RelDecl.get_name decl with
@@ -605,7 +606,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     user_err Pp.(str "Priorities only allowed for type class substructures");
   (* Now, younger decl in params and fields is on top *)
-  let (pl, ctx), arity, template, implpars, params, implfs, fields =
+  let pl, ctx, arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
       typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 62c7edb19..e2f28a371 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1555,8 +1555,8 @@ 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 ~names:[] ~extensible:true sigma' in
-  let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
+  let uctx = Evd.universe_context_set sigma' in
+  let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
     if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
@@ -1572,7 +1572,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
 	Feedback.msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
-                    Printer.pr_universe_ctx sigma uctx)
+                    Printer.pr_universe_ctx_set sigma uctx)
     | Some r ->
         let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
 	let redfun env evm c =