From d37aab528dca587127b9f9944e1521e4fc3d9cc7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 7 Oct 2015 13:11:52 +0200
Subject: 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.
---
 intf/misctypes.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf')

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
-- 
cgit v1.2.3