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

5 files changed, 14 insertions, 11 deletions

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"];