Univs: add Strict Universe Declaration option (on by default)

This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.

35 files changed, 104 insertions, 26 deletions

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 74e136904d..5c11119ed8 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -44,8 +44,8 @@ type 'id move_location =
 (** Sorts *)
 
 type 'a glob_sort_gen = GProp | GSet | GType of 'a
-type sort_info = string list
-type level_info = string option
+type sort_info = string Loc.located list
+type level_info = string Loc.located option
 
 type glob_sort = sort_info glob_sort_gen
 type glob_level = level_info glob_sort_gen
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e47e3fb1e6..9fe3022341 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -153,12 +153,12 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+      | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
       ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
-      | id = ident -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
+      | id = identref -> [id]
       ] ]
   ;
   lconstr:
@@ -302,7 +302,7 @@ GEXTEND Gram
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | id = ident -> GType (Some (Id.to_string id))
+      | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
       ] ]
   ;
   fix_constr:
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8bd57290b0..a1213e72be 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -401,7 +401,7 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
+       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -413,7 +413,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
+  GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4e0b6f75e7..4372668fcf 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1074,12 +1074,6 @@ let uctx_new_univ_variable rigid name predicative
 	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
 	else {uctx with uctx_univ_variables = uvars'}, false
   in
-  (* let ctx' = *)
-  (*   if pred then *)
-  (*     Univ.ContextSet.add_constraints *)
-  (* 	(Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *)
-  (*   else ctx' *)
-  (* in *)
   let names = 
     match name with
     | Some n -> add_uctx_names n u uctx.uctx_names
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 0926e7a299..a0ec1baae2 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.equal CString.equal l1 l2
+| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2efd8fe413..dec23328f4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -99,8 +99,22 @@ let search_guard loc env possible_indexes fixdefs =
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
+(* To force universe name declaration before use *)
+
+let strict_universe_declarations = ref true
+let is_strict_universe_declarations () = !strict_universe_declarations
+
+let _ =
+  Goptions.(declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "strict universe declaration";
+	    optkey   = ["Strict";"Universe";"Declaration"];
+	    optread  = is_strict_universe_declarations;
+	    optwrite = (:=) strict_universe_declarations })
+						  
 (** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd s =
+let interp_universe_level_name evd (loc,s) =
   let names, _ = Universes.global_universe_names () in
     if CString.string_contains s "." then
       match List.rev (CString.split '.' s) with
@@ -122,7 +136,10 @@ let interp_universe_level_name evd s =
 	try let level = Evd.universe_of_name evd s in
 	      evd, level
 	with Not_found -> 
-	  new_univ_level_variable ~name:s univ_rigid evd
+	  if not (is_strict_universe_declarations ()) then
+  	    new_univ_level_variable ~name:s univ_rigid evd
+	  else user_err_loc (loc, "interp_universe_level_name",
+			     Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe evd = function
   | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
@@ -135,7 +152,7 @@ let interp_universe evd = function
 
 let interp_universe_level evd = function
   | None -> new_univ_level_variable univ_rigid evd
-  | Some s -> interp_universe_level_name evd s
+  | Some (loc,s) -> interp_universe_level_name evd (loc,s)
 
 let interp_sort evd = function
   | GProp -> evd, Prop Null
@@ -357,7 +374,8 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_universe_level_name evd = function
+let interp_universe_level_name evd l =
+  match l with
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_universe_level evd s
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 650b8f7262..ea705e335e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -140,8 +140,8 @@ end) = struct
 
   let pr_univ l =
     match l with
-      | [x] -> str x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+      | [_,x] -> str x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -174,7 +174,7 @@ end) = struct
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some u -> str u
+        | Some (_,u) -> str u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index 4cd7c39e88..e6a50449da 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v
index b57b0a0f0b..f8113e4c78 100644
--- a/test-suite/bugs/closed/3352.v
+++ b/test-suite/bugs/closed/3352.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 (*
 I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo].  (I think this worked in HoTT/coq, too.)  Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A].  (The issue is tricker when IsHProp uses [A] elsewhere, as in:
diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v
index 0e236c2172..b8bb8bce09 100644
--- a/test-suite/bugs/closed/3386.v
+++ b/test-suite/bugs/closed/3386.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v
index ae212caa5d..cb435e7865 100644
--- a/test-suite/bugs/closed/3387.v
+++ b/test-suite/bugs/closed/3387.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index 50645090fa..da12b68689 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 8657 lines to
 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines,
 then from 51 lines to 37 lines, then from 43 lines to 30 lines *)
diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v
index b2aa8c3cd6..e2d7976981 100644
--- a/test-suite/bugs/closed/3566.v
+++ b/test-suite/bugs/closed/3566.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Notation idmap := (fun x => x).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
 Arguments idpath {A a} , [A] a.
diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v
index a5b0e9347d..e69ec10976 100644
--- a/test-suite/bugs/closed/3666.v
+++ b/test-suite/bugs/closed/3666.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index 4069e38075..df9f5f4761 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
index b9b2dd6b3e..e203528fcc 100644
--- a/test-suite/bugs/closed/3777.v
+++ b/test-suite/bugs/closed/3777.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module WithoutPoly.
   Unset Universe Polymorphism.
   Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v
index eb0d206c5c..2b44e225e8 100644
--- a/test-suite/bugs/closed/3779.v
+++ b/test-suite/bugs/closed/3779.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
 Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
index 6e19ddf8dc..a5c84e6856 100644
--- a/test-suite/bugs/closed/3808.v
+++ b/test-suite/bugs/closed/3808.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
   := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
index 8da4f73626..30261ed266 100644
--- a/test-suite/bugs/closed/3821.v
+++ b/test-suite/bugs/closed/3821.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
 
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 0ccc92067d..5013bc6ac1 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Notation Type0 := Set.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index c6cb9c35e6..e4d76732a3 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index 5f8c411ca8..d34a2b8b1b 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index e139c5b6c9..0623cf5b84 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 Universe b.
 
diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v
new file mode 100644
index 0000000000..955c3017d7
--- /dev/null
+++ b/test-suite/bugs/closed/4299.v
@@ -0,0 +1,12 @@
+Unset Strict Universe Declaration.
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type : Type.
+  Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type : Type.
+  Definition U := let X := Type in Type.
+  Definition eq : Type = U := eq_refl.
+Fail End M.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
index 3b00efb213..b4e17c2231 100644
--- a/test-suite/bugs/closed/4301.v
+++ b/test-suite/bugs/closed/4301.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 
 Module Type Foo.
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
index 0b8bb23534..844ff87566 100644
--- a/test-suite/bugs/closed/HoTT_coq_007.v
+++ b/test-suite/bugs/closed/HoTT_coq_007.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Module Comment1.
   Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index 4c3e078a50..7a84531a77 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module Version1.
   Set Implicit Arguments.
   Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
index b7db22a69e..90d1d18306 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
index f382dac976..4f8868d538 100644
--- a/test-suite/bugs/closed/HoTT_coq_093.v
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
 Set Printing All.
 Set Printing Implicit.
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index 9b3f94d917..a717bbe735 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 059462fac3..f9154ef576 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -4,6 +4,8 @@
 (* Fail  exact H. *)
 (* Section . *)
 
+Unset Strict Universe Declaration.
+
 Section lift_strict.
 Polymorphic Definition liftlt := 
   let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 957612ef1d..d6bbfe29ac 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,5 @@
+Unset Strict Universe Declaration.
+
 Module withoutpoly.
 
 Inductive empty :=. 
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v
new file mode 100644
index 0000000000..31d264f645
--- /dev/null
+++ b/test-suite/success/univnames.v
@@ -0,0 +1,26 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A.
+
+Set Printing Universes.
+
+Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A.
+
+Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type.
+
+Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type.
+
+Definition nothing (A : Type) := A.
+
+Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
+
+Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
+
+
+Universe g.
+
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9d3952e64a..fdedbf672a 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -266,8 +266,10 @@ Section GenericInstances.
     transitivity (y x0)...
   Qed.
 
+  Unset Strict Universe Declaration.
+  
   (** The complement of a crelation conserves its proper elements. *)
-  Program Definition complement_proper
+  Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
           `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
     Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
   
@@ -279,7 +281,6 @@ Section GenericInstances.
   Qed.
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
-
   Program Definition flip_proper
           `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
     Proper (RB ==> RA ==> RC) (flip f) := _.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b65ff73feb..285baf3f97 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -500,12 +500,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
-  let evdref = ref Evd.(from_env env0) in
+  let pl = (List.hd indl).ind_univs in
+  let ctx = Evd.make_evar_universe_context env0 pl in
+  let evdref = ref Evd.(from_ctx ctx) in
   let _, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-  let pl = (List.hd indl).ind_univs in
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in