diff options
| author | Matthieu Sozeau | 2016-09-28 17:26:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-20 17:39:00 +0200 |
| commit | 474a58b15ca41f1b3287ef3e29e80cca9988598c (patch) | |
| tree | 52446a501765d6185a9b42e737f3d3f7c6ef2b18 /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 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520bc..db7318469f 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,7 +263,10 @@ 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 (** This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) + (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 |