Merge PR #12653: Syntax for specifying cumulative inductives

Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot

1 files changed, 23 insertions, 2 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 02c3c047d5..0eb915561e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2648,13 +2648,34 @@ let interp_univ_decl env decl =
   let binders : lident list = decl.univdecl_instance in
   let evd = Evd.from_env ~binders env in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = binders;
+  let decl = {
+    univdecl_instance = binders;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;
-    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+  }
   in evd, decl
 
+let interp_cumul_univ_decl env decl =
+  let open UState in
+  let binders = List.map fst decl.univdecl_instance in
+  let variances = Array.map_of_list snd decl.univdecl_instance in
+  let evd = Evd.from_ctx (UState.from_env ~binders env) in
+  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+  let decl = {
+    univdecl_instance = binders;
+    univdecl_extensible_instance = decl.univdecl_extensible_instance;
+    univdecl_constraints = cstrs;
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+  }
+  in
+  evd, decl, variances
+
 let interp_univ_decl_opt env l =
   match l with
   | None -> Evd.from_env env, UState.default_univ_decl
   | Some decl -> interp_univ_decl env decl
+
+let interp_cumul_univ_decl_opt env = function
+  | None -> Evd.from_env env, UState.default_univ_decl, [| |]
+  | Some decl -> interp_cumul_univ_decl env decl