diff options
| author | Matthieu Sozeau | 2015-11-27 17:21:10 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-27 17:23:04 +0100 |
| commit | 8297baa98147f78263126b1bd6cf41b0456f177d (patch) | |
| tree | a8edc484c3ff79af76d02dce80fca5f1b27d00ef | |
| parent | 982460743a54ecfab1d601ba930d61c04972d17a (diff) | |
Fix [Polymorphic Hint Rewrite].
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index cab74968d2..9ffcd2dcff 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -264,7 +264,7 @@ TACTIC EXTEND rewrite_star let add_rewrite_hint bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in - let poly = Flags.is_universe_polymorphism () in + let poly = Flags.use_polymorphic_flag () in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 177c3fb0ab..2b23323248 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2048,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). *) @@ -2149,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 @@ -2161,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) |