diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-20 17:45:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-20 17:45:17 +0200 |
| commit | 3e536acf2ebcd078314dcac2a79d267c95db7bf8 (patch) | |
| tree | 39372d99951e30f1429b1d45a0a0844d9db8b588 /ltac | |
| parent | df1de9fa318f1924d92fb39c4bc67c16f3d31db4 (diff) | |
| parent | 474a58b15ca41f1b3287ef3e29e80cca9988598c (diff) | |
Merge branch 'bug5036' into v8.6
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d6ba670d8..db7318469 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 |