summaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
commit164c6861860e6b52818c031f901ffeff91fca16a (patch)
tree4f91d20c890c25915e7b28226c663b94a8cfb0d3 /toplevel/vernacentries.ml
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml21
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)