Imported Upstream version 8.5upstream/8.5

1 files changed, 10 insertions, 11 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b6a1a53f..72dd967b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -355,11 +355,6 @@ let dump_universes_gen g s =
     close ();
     iraise reraise
 
-let dump_universes sorted s =
-  let g = Global.universes () in
-  let g = if sorted then Univ.sort_universes g else g in
-  dump_universes_gen g s
-
 (*********************)
 (* "Locate" commands *)
 
@@ -1623,15 +1618,17 @@ let vernac_print = function
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
   | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
-  | PrintUniverses (b, None) ->
+  | PrintUniverses (b, dst) ->
      let univ = Global.universes () in
      let univ = if b then Univ.sort_universes univ else univ in
      let pr_remaining =
        if Global.is_joined_environment () then mt ()
        else str"There may remain asynchronous universe constraints"
      in
-     msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
-  | PrintUniverses (b, Some s) -> dump_universes b s
+     begin match dst with
+     | None -> msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
+     | Some s -> dump_universes_gen univ s
+     end
   | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
   | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
@@ -2051,7 +2048,7 @@ let check_vernac_supports_polymorphism c p =
 
 let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
-  | Some b -> b
+  | Some b -> Flags.make_polymorphic_flag b; b
 
 (** A global default timeout, controled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2152,7 +2149,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             then Flags.verbosely (interp ?proof ~loc locality poly) c
             else Flags.silently  (interp ?proof ~loc locality poly) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
-            Flags.program_mode := orig_program_mode
+            Flags.program_mode := orig_program_mode;
+	  ignore (Flags.use_polymorphic_flag ())
           end
         with
         | reraise when
@@ -2164,6 +2162,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             let e = locate_if_not_already loc e in
             let () = restore_timeout () in
             Flags.program_mode := orig_program_mode;
+	    ignore (Flags.use_polymorphic_flag ());
             iraise e
   and aux_list ?locality ?polymorphism isprogcmd l =
     List.iter (aux false) (List.map snd l)