diff options
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 49e8588da3..f765318d04 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,7 +12,7 @@ open Term open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option +type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -56,7 +56,7 @@ type hypinfo = { hyp_right : constr; } -val find_applied_relation : bool -> - Loc.t -> +val find_applied_relation : + ?loc:Loc.t -> bool -> Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo |