diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 3 |
2 files changed, 8 insertions, 3 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 23ce5fb4ea..8ea60b39ae 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -262,8 +262,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 @@ -352,7 +354,7 @@ let refine_tac ist simple c = let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in - let refine = Refine.refine ~unsafe:false update in + let refine = Refine.refine ~unsafe:true update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 92a403c585..e927ea0642 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -866,6 +866,9 @@ let rec message_of_value v = Ftactic.return (pr_closed_glob_env (pf_env gl) (project gl) c) end } + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_id id) end } else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> |