Merge branch 'v8.5'

4 files changed, 12 insertions, 16 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 c92c8fff76..15065afdae 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
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bc8aa2fffa..966b952016 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -215,7 +215,7 @@ let display_cmd_header loc com =
 	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com verbose checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
@@ -241,7 +241,7 @@ let rec vernac_com checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
+    | v -> Stm.interp verbose (loc,v)
   in
     try
       checknav loc com;
@@ -268,7 +268,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com checknav loc_ast;
+      vernac_com verbosely checknav loc_ast;
       pp_flush ()
     done
   with any ->   (* whatever the exception *)
@@ -293,7 +293,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =