diff options
| -rw-r--r-- | library/declare.ml | 6 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 6 |
2 files changed, 8 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index c5b83c11a0..c9992fff3b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -491,8 +491,10 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in - cache_universe_context (p,ctx) + let ctx = + Univ.ContextSet.add_constraints c + Univ.ContextSet.empty (* No declared universes here, just constraints *) + in cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d6ba670d83..db7318469f 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,8 +263,10 @@ let add_rewrite_hint bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (Declare.declare_universe_context 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 |