From f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2020 14:01:00 +0200
Subject: Make explicit that UGraph lower bounds are only of two kinds.

This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
---
 vernac/comInductive.ml | 2 +-
 vernac/record.ml       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index cc9b840bed..4242f06844 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* In case of template polymorphism, we need to compute more constraints *)
-  let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+  let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
 
   let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
     interp_params env0 udecl uparamsl paramsl
diff --git a/vernac/record.ml b/vernac/record.ml
index 9fda98d08e..36254780cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records =
      any Set <= i constraint for universes that might actually be instantiated with Prop. *)
   let is_template =
     List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
-  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
+  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =
-- 
cgit v1.2.3