diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520bc..d6ba670d83 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,7 +263,8 @@ let add_rewrite_hint bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (Global.push_context_set false ctx; Univ.ContextSet.empty) + else (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in let eqs = List.map f lcsr in |