3 files changed, 9 insertions, 15 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 0bce22f584..d4be81c61a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -87,8 +87,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let xml_export = ref false
-
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
@@ -96,7 +94,6 @@ let time = ref false
 
 let raw_print = ref false
 
-
 let univ_print = ref false
 
 let we_are_parsing = ref false
@@ -167,9 +164,9 @@ let use_polymorphic_flag () =
 let make_polymorphic_flag b =
   local_polymorphic_flag := Some b
 
-let inductive_cumulativity = ref false
-let make_inductive_cumulativity b = inductive_cumulativity := b
-let is_inductive_cumulativity () = !inductive_cumulativity
+let polymorphic_inductive_cumulativity = ref false
+let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
+let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
 
 (** [program_mode] tells that Program mode has been activated, either
     globally via [Set Program] or locally via the Program command prefix. *)
diff --git a/lib/flags.mli b/lib/flags.mli
index eb4c37a548..3024c60396 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -56,11 +56,6 @@ val stm_debug : bool ref
 
 val profile : bool
 
-(* Legacy flags *)
-
-(* -xml option: xml hooks will be called *)
-val xml_export : bool ref
-
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
@@ -119,9 +114,9 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
-(** Global inductive cumulativity flag. *)
-val make_inductive_cumulativity : bool -> unit
-val is_inductive_cumulativity : unit -> bool
+(** Global polymorphic inductive cumulativity flag. *)
+val make_polymorphic_inductive_cumulativity : bool -> unit
+val is_polymorphic_inductive_cumulativity : unit -> bool
 
 val warn : bool ref
 val make_warn : bool -> unit
diff --git a/lib/minisys.ml b/lib/minisys.ml
index 1ed017e489..706f0430c3 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -44,11 +44,13 @@ let ok_dirname f =
 (* Check directory can be opened *)
 
 let exists_dir dir =
+  (* See BZ#5391 on windows failing on a trailing (back)slash *)
   let rec strip_trailing_slash dir =
     let len = String.length dir in
     if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
     then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
-  try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
+  let dir = if Sys.os_type = "Win32" then strip_trailing_slash dir else dir in
+  try Sys.is_directory dir with Sys_error _ -> false
 
 let apply_subdir f path name =
   (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)