1 files changed, 75 insertions, 8 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 05c40dbdd7..629fcce5a7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -29,7 +29,6 @@ open Indtypes
 open Pretyping
 open Evarutil
 open Indschemes
-open Misctypes
 open Context.Rel.Declaration
 open Entries
 
@@ -178,6 +177,72 @@ let is_flexible_sort evd u =
   | Some l -> Evd.is_flexible_level evd l
   | None -> false
 
+(**********************************************************************)
+(* Tools for template polymorphic inductive types                         *)
+
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur only in the le constraints *)
+
+(*
+   Solve a system of universe constraint of the form
+
+   u_s11, ..., u_s1p1, w1 <= u1
+   ...
+   u_sn1, ..., u_snpn, wn <= un
+
+where
+
+  - the ui (1 <= i <= n) are universe variables,
+  - the sjk select subsets of the ui for each equations,
+  - the wi are arbitrary complex universes that do not mention the ui.
+*)
+
+let is_direct_sort_constraint s v = match s with
+  | Some u -> Univ.univ_level_mem u v
+  | None -> false
+
+let solve_constraints_system levels level_bounds =
+  let open Univ in
+  let levels =
+    Array.mapi (fun i o ->
+      match o with
+      | Some u ->
+        (match Universe.level u with
+        | Some u -> Some u
+        | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+      | None -> None)
+      levels in
+  let v = Array.copy level_bounds in
+  let nind = Array.length v in
+  let clos = Array.map (fun _ -> Int.Set.empty) levels in
+  (* First compute the transitive closure of the levels dependencies *)
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
+        clos.(i) <- Int.Set.add j clos.(i);
+    done;
+  done;
+  let rec closure () =
+    let continue = ref false in
+      Array.iteri (fun i deps ->
+        let deps' =
+          Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
+        in
+          if Int.Set.equal deps deps' then ()
+          else (clos.(i) <- deps'; continue := true))
+        clos;
+      if !continue then closure ()
+      else ()
+  in
+  closure ();
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
+        (v.(i) <- Universe.sup v.(i) level_bounds.(j));
+    done;
+  done;
+  v
+
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
@@ -206,8 +271,8 @@ let inductive_levels env evd poly arities inds =
   in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
-  let levels' = Universes.solve_constraints_system (Array.of_list levels)
-    (Array.of_list cstrs_levels) (Array.of_list min_levels)
+  let levels' = solve_constraints_system (Array.of_list levels)
+    (Array.of_list cstrs_levels)
   in
   let evd, arities =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
@@ -304,14 +369,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   (* Try further to solve evars, and instantiate them *)
   let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
   (* Compute renewed arities *)
-  let sigma, nf = nf_evars_and_universes sigma in
+  let sigma = Evd.minimize_universes sigma in
+  let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
   let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
-  let sigma, nf' = nf_evars_and_universes sigma in
-  let arities = List.map nf' arities in
-  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
+  let sigma = Evd.minimize_universes sigma in
+  let nf = Evarutil.nf_evars_universes sigma in
+  let arities = List.map nf arities in
+  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
   List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
@@ -378,7 +445,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
     ind_name = indname; ind_univs = pl;
-    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar;
+    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar;
     ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
   }) indl