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 /tactics | |
| parent | 982460743a54ecfab1d601ba930d61c04972d17a (diff) | |
Fix [Polymorphic Hint Rewrite].
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
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 = |