diff options
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 07065717..03e9414e 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,19 +1,20 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files implements the autorewrite tactic. *) -open Term -open Tacexpr +open Constr 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) CAst.t (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -29,7 +30,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_ctx: Univ.ContextSet.t; rew_l2r: bool; rew_tac: Genarg.glob_generic_argument option } @@ -41,7 +42,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : string -> Pp.std_ppcmds +val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t open Clenv @@ -57,7 +58,7 @@ type hypinfo = { hyp_right : constr; } -val find_applied_relation : bool -> - Loc.t -> - Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo +val find_applied_relation : + ?loc:Loc.t -> bool -> + Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo |