diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 01:13:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
| commit | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (patch) | |
| tree | 7defb39c88bdf0d163ca323955d11f1a50d2367d /checker/checker.ml | |
| parent | 591e7e484d544e958595a0fb784336ae050a9c74 (diff) | |
Option -type-in-type: added support in checker and making it contaminating
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 0f7ed8df5..d5d9b9e3b 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -138,10 +138,11 @@ let init_load_path () = let set_debug () = Flags.debug := true -let engagement = ref None -let set_engagement c = engagement := Some c -let engage () = - match !engagement with Some c -> Safe_typing.set_engagement c | None -> () +let impredicative_set = ref Cic.PredicativeSet +let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet +let type_in_type = ref Cic.StratifiedType +let set_type_in_type () = type_in_type := Cic.TypeInType +let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type) let admit_list = ref ([] : section_path list) @@ -194,6 +195,7 @@ let print_usage_channel co command = \n -silent disable trace of constants being checked\ \n\ \n -impredicative-set set sort Set impredicative\ +\n -type-in-type collapse type hierarchy\ \n\ \n -h, --help print this list of options\ \n" @@ -319,7 +321,9 @@ let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> - set_engagement Cic.ImpredicativeSet; parse rem + set_impredicative_set (); parse rem + | "-type-in-type" :: rem -> + set_type_in_type (); parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then |