diff options
| author | Hugo Herbelin | 2015-07-10 01:13:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-10 19:18:41 +0200 |
| commit | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (patch) | |
| tree | 7defb39c88bdf0d163ca323955d11f1a50d2367d /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 15 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
3 files changed, 8 insertions, 12 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 77339aef44..04238da2bd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -360,8 +360,7 @@ let make_conclusion_flexible evdref ty poly = else () let is_impredicative env u = - u = Prop Null || - (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos) + u = Prop Null || (is_impredicative_set env && u = Prop Pos) let interp_ind_arity env evdref ind = let c = intern_gen IsType env ind.ind_arity in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5b330cd252..5540dc0ff1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -112,14 +112,12 @@ let print_memory_stat () = let _ = at_exit print_memory_stat -let engagement = ref None -let set_engagement c = engagement := Some c +let impredicative_set = ref Declarations.PredicativeSet +let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet +let type_in_type = ref Declarations.StratifiedType +let set_type_in_type () = type_in_type := Declarations.TypeInType let engage () = - match !engagement with Some c -> Global.set_engagement c | None -> () - -let type_in_type = ref false -let set_type_in_type () = type_in_type := true -let set_hierarchy () = if !type_in_type then Global.set_type_in_type () + Global.set_engagement (!impredicative_set,!type_in_type) let set_batch_mode () = batch_mode := true @@ -521,7 +519,7 @@ let parse_args arglist = |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true - |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet + |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> Vernac.just_parsing := true |"-m"|"--memory" -> memory_stat := true @@ -605,7 +603,6 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); - set_hierarchy (); (* Be careful to set these variables after the inputstate *) Syntax_def.set_verbose_compat_notations !verb_compat_ntn; Syntax_def.set_compat_notations (not !no_compat_ntn); diff --git a/toplevel/record.ml b/toplevel/record.ml index 737b7fb59f..15ad18d9cc 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -135,7 +135,7 @@ let typecheck_params_and_fields def id t ps nots fs = let ctx, aritysort = Reduction.dest_arity env0 arity in assert(List.is_empty ctx); (* Ensured by above analysis *) if Sorts.is_prop aritysort || - (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then + (Sorts.is_set aritysort && is_impredicative_set env0) then evars else Evd.set_leq_sort env_ar evars (Type univ) aritysort in |