Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 45 insertions, 12 deletions

diff --git a/tactics/equality.mli b/tactics/equality.mli
index ab439c39..3e4bfed7 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -6,7 +6,7 @@
 (*         *       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 $Id: equality.mli 8651 2006-03-21 21:54:43Z jforest $ i*)
 
 (*i*)
 open Names
@@ -24,24 +24,34 @@ 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
 
+(* Obsolete, use [general_rewrite_bindings l2r]
+[val rewriteLR_bindings       : constr with_bindings -> tactic]
+[val rewriteRL_bindings       : constr with_bindings -> tactic]
+*)
+
+(* Equivalent to [general_rewrite l2r] *)
 val rewriteLR   : constr -> tactic
 val rewriteRL   : constr  -> tactic
 
+(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
+
+val general_rewrite_bindings_in :
+  bool -> identifier -> constr with_bindings -> tactic
+val general_rewrite_in          :
+  bool -> identifier -> 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 replace_by : constr -> constr -> tactic -> tactic 
+val replace_in_by : identifier -> constr -> constr -> tactic -> tactic 
+val new_replace : constr -> constr -> identifier option -> tactic option -> tactic
 val discr        : identifier -> tactic
 val discrConcl   : tactic
 val discrClause  : clause -> tactic
@@ -55,15 +65,38 @@ 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
+  env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
 
+(* The family cutRewriteIn expect an equality statement *)
+val cutRewriteInHyp : bool -> types -> identifier -> tactic
+val cutRewriteInConcl : bool -> constr -> tactic
+
+(* The family rewriteIn expect the proof of an equality *)
+val rewriteInHyp : bool -> constr -> identifier -> tactic
+val rewriteInConcl : bool -> constr -> tactic
+
+(* Expect the proof of an equality; fails with raw internal errors *)
+val substClause : bool -> constr -> identifier option -> tactic
+
+(*
+(* [substHypInConcl l2r id] is obsolete: use [rewriteInConcl l2r (mkVar id)] *)
 val substHypInConcl : bool -> identifier -> tactic
+
+(* [substConcl] is an obsolete synonym for [cutRewriteInConcl] *)
 val substConcl : bool -> constr -> tactic
-val substHyp : bool -> constr -> identifier -> tactic
 
-val hypSubst_LR : identifier -> clause -> tactic
-val hypSubst_RL : identifier -> clause -> tactic
+(* [substHyp] is an obsolete synonym of [cutRewriteInHyp] *)
+val substHyp : bool -> types -> identifier -> tactic
+*)
+
+(* Obsolete, use [rewriteInConcl lr (mkVar id)] in concl
+              or [rewriteInHyp lr (mkVar id) (Some hyp)] in hyp
+   (which, if they fail, raise only UserError, not PatternMatchingFailure)
+   or [substClause lr (mkVar id) None]
+   or [substClause lr (mkVar id) (Some hyp)]
+[val hypSubst_LR : identifier -> clause -> tactic]
+[val hypSubst_RL : identifier -> clause -> tactic]
+*)
 
 val discriminable : env -> evar_map -> constr -> constr -> bool