aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/extratactics.ml42
1 files changed, 1 insertions, 1 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 =