diff options
| author | jforest | 2006-03-21 21:54:43 +0000 |
|---|---|---|
| committer | jforest | 2006-03-21 21:54:43 +0000 |
| commit | dfa81d7860309029d100cd5348d2dd6bd8fa33c9 (patch) | |
| tree | 6421299af0b72711fff483052951dee4b0e53fa1 /tactics/equality.mli | |
| parent | b8a287758030a451cf758f3b52ec607a8196fba1 (diff) | |
+ destruct now works as induction on multiple arguments :
destruct x y z using scheme
+ replace c1 with c2 <in hyp> has now a new optional argument <as tac>
replace c1 with c2 by tac tries to prove c2 = c1 with tac
+ I've also factorize the code correspoing to replace in extractactics
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index fc7c3828ea..7632fd36bd 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -49,7 +49,9 @@ val conditional_rewrite_in : 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 |