diff options
| author | Matthieu Sozeau | 2016-09-28 17:26:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-29 17:49:43 +0200 |
| commit | cf87e73ff4dd0b9c70436d66d326ae839868ba78 (patch) | |
| tree | 1df8eeecc54c7cc1cf30af8a31800e3f694eaad9 /ltac | |
| parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) | |
Fix bug #5036 autorewrite, sections and universes
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
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 |