diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 46fb55b5f..e34f38eb3 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -115,10 +115,11 @@ let _ = at_exit print_memory_stat 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 set_type_in_type () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_universes = false } let engage () = - Global.set_engagement (!impredicative_set,!type_in_type) + Global.set_engagement !impredicative_set let set_batch_mode () = batch_mode := true |