diff options
| author | Matthieu Sozeau | 2015-10-07 13:11:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-07 13:17:11 +0200 |
| commit | d37aab528dca587127b9f9944e1521e4fc3d9cc7 (patch) | |
| tree | 3d8db828b3e6644c924a75592dded2a168fbeb59 /pretyping/pretyping.ml | |
| parent | 840155eafd9607c7656c80770de1e2819fe56a13 (diff) | |
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.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 26 |
1 files changed, 22 insertions, 4 deletions
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 |