diff options
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 198fa36f5..046291135 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -11,7 +11,7 @@ open Tacexpr open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr option +type raw_rew_rule = Loc.t * Term.constr Univ.in_universe_context_set * bool * Tacexpr.raw_tactic_expr option (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -27,6 +27,7 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic -> type rew_rule = { rew_lemma: constr; rew_type: types; rew_pat: constr; + rew_ctx: Univ.universe_context_set; rew_l2r: bool; rew_tac: glob_tactic_expr option } |