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.

4 files changed, 25 insertions, 13 deletions

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