diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-12 19:36:15 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 11:52:57 +0100 |
commit | 05fc0542f6c7a15b9187a2a91beb0aa7a42bb2fa (patch) | |
tree | 97eccce3247c2d6d79d9b3cde4bc86410bd1d02c /vernac/vernacentries.ml | |
parent | 2a25e1a56460556f8b8dcef2a70cd0d2b9422383 (diff) |
Remove the local polymorphic flag hack.
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r-- | vernac/vernacentries.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index aa6121c39..270e440e1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2132,10 +2132,6 @@ let check_vernac_supports_polymorphism c p = | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") -let enforce_polymorphism = function - | None -> Flags.is_universe_polymorphism () - | Some b -> Flags.make_polymorphic_flag b; b - (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2202,6 +2198,7 @@ let with_fail st b f = end let interp ?(verbosely=true) ?proof ~st (loc,c) = + let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in let rec control = function | VernacExpr v -> @@ -2241,7 +2238,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | c -> check_vernac_supports_locality c atts.locality; check_vernac_supports_polymorphism c polymorphism; - let polymorphic = enforce_polymorphism polymorphism in + let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in + Flags.make_universe_polymorphism polymorphic; Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> @@ -2249,9 +2247,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = if verbosely then Flags.verbosely (interp ?proof ~atts ~st) c else Flags.silently (interp ?proof ~atts ~st) c; + (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`, + we should not restore the previous state of the flag... *) if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()) + if (Flags.is_universe_polymorphism() = polymorphic) then + Flags.make_universe_polymorphism orig_univ_poly; end with | reraise when @@ -2262,8 +2263,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = let e = CErrors.push reraise in let e = locate_if_not_already ?loc e in let () = restore_timeout () in + Flags.make_universe_polymorphism orig_univ_poly; Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()); iraise e in if verbosely |