diff options
| author | Matthieu Sozeau | 2016-09-29 17:50:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-29 17:50:09 +0200 |
| commit | fdfcdc79989c46737089e4c8cab5ad0090e4d8a6 (patch) | |
| tree | 6a998ec6f6f641343e86d330a5d17c40866c01a6 /ltac | |
| parent | 2a13b37356cb87de737eaf72b60f337c90913ef9 (diff) | |
| parent | cf87e73ff4dd0b9c70436d66d326ae839868ba78 (diff) | |
Merge branch 'bug5036' into v8.6
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 |