New datastructure for universes of inductive types

1 files changed, 20 insertions, 0 deletions

diff --git a/engine/universes.ml b/engine/universes.ml
index f20108186..955e1d8b5 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -1118,3 +1118,23 @@ let solve_constraints_system levels level_bounds level_min =
     done;
   done;
   v
+
+
+(** Operations for universe_info_ind *)
+
+(** Given a universe context representing constraints of an inductive
+    this function produces a UInfoInd.t that with the trivial subtyping relation. *)
+let univ_inf_ind_from_universe_context univcst =
+  let freshunivs = Instance.of_array
+      (Array.map (fun _ -> new_univ_level ())
+         (Instance.to_array (UContext.instance univcst)))
+  in UInfoInd.from_universe_context univcst freshunivs
+
+(** This function adds universe constraints to the universe
+    constraints of the given universe_info_ind. However one must be
+    CAUTIOUS as it resets the subtyping constraints to equality. *)
+let univ_inf_ind_union uinfind univcst' =
+  let freshunivs = Instance.of_array
+      (Array.map (fun _ -> new_univ_level ())
+         (Instance.to_array (UContext.instance univcst')))
+  in UInfoInd.union uinfind univcst' freshunivs