diff options
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 |