diff options
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 750addcc..eb71f68e 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: setoid_replace.mli 8779 2006-05-02 20:59:21Z letouzey $ i*) +(*i $Id: setoid_replace.mli 9073 2006-08-22 08:54:29Z jforest $ i*) open Term open Proof_type @@ -39,7 +39,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds -val register_replace : (constr -> constr -> tactic) -> unit +val register_replace : (tactic option -> constr -> constr -> tactic) -> unit val register_general_rewrite : (bool -> constr -> tactic) -> unit val print_setoids : unit -> unit @@ -52,8 +52,9 @@ val default_morphism : ?filter:(constr morphism -> bool) -> constr -> relation morphism val setoid_replace : - constr option -> constr -> constr -> new_goals:constr list -> tactic + tactic option -> constr option -> constr -> constr -> new_goals:constr list -> tactic val setoid_replace_in : + tactic option -> identifier -> constr option -> constr -> constr -> new_goals:constr list -> tactic |