diff options
Diffstat (limited to 'tactics/equality.mli')
-rw-r--r-- | tactics/equality.mli | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli new file mode 100644 index 00000000..ab439c39 --- /dev/null +++ b/tactics/equality.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: equality.mli,v 1.26.2.1 2004/07/16 19:30:53 herbelin Exp $ i*) + +(*i*) +open Names +open Term +open Sign +open Evd +open Environ +open Proof_type +open Tacmach +open Hipattern +open Pattern +open Tacticals +open Tactics +open Tacexpr +open Rawterm +(*i*) + +val find_eq_pattern : sorts -> sorts -> constr + +val general_rewrite_bindings : bool -> constr with_bindings -> tactic +val general_rewrite : bool -> constr -> tactic +val rewriteLR_bindings : constr with_bindings -> tactic +val rewriteRL_bindings : constr with_bindings -> tactic + +val rewriteLR : constr -> tactic +val rewriteRL : constr -> tactic + +val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic +val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic +val conditional_rewrite_in : + bool -> identifier -> tactic -> constr with_bindings -> tactic + +val replace : constr -> constr -> tactic +val replace_in : identifier -> constr -> constr -> tactic + +val discr : identifier -> tactic +val discrConcl : tactic +val discrClause : clause -> tactic +val discrHyp : identifier -> tactic +val discrEverywhere : tactic +val discr_tac : quantified_hypothesis option -> tactic +val inj : identifier -> tactic +val injClause : quantified_hypothesis option -> tactic + +val dEq : quantified_hypothesis option -> tactic +val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic + +val make_iterated_tuple : + env -> evar_map -> (constr * constr) -> (constr * constr) + -> constr * constr * constr + +val substHypInConcl : bool -> identifier -> tactic +val substConcl : bool -> constr -> tactic +val substHyp : bool -> constr -> identifier -> tactic + +val hypSubst_LR : identifier -> clause -> tactic +val hypSubst_RL : identifier -> clause -> tactic + +val discriminable : env -> evar_map -> constr -> constr -> bool + +(* Subst *) + +val unfold_body : identifier -> tactic + +val subst : identifier list -> tactic +val subst_all : tactic + +(* Replace term *) +val replace_term_left : constr -> tactic +val replace_term_right : constr -> tactic +val replace_term : constr -> tactic +val replace_term_in_left : constr -> identifier -> tactic +val replace_term_in_right : constr -> identifier -> tactic +val replace_term_in : constr -> identifier -> tactic |