diff options
| author | Matthieu Sozeau | 2016-10-20 17:45:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-20 17:45:17 +0200 |
| commit | 3e536acf2ebcd078314dcac2a79d267c95db7bf8 (patch) | |
| tree | 39372d99951e30f1429b1d45a0a0844d9db8b588 | |
| parent | df1de9fa318f1924d92fb39c4bc67c16f3d31db4 (diff) | |
| parent | 474a58b15ca41f1b3287ef3e29e80cca9988598c (diff) | |
Merge branch 'bug5036' into v8.6
| -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 |