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 /parsing/pptactic.ml | |
| 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 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9ec4dfd03c..a90e001f5d 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -691,7 +691,8 @@ and pr_atom1 env = function hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) | TacNewDestruct (h,e,ids) -> hov 1 (str "destruct" ++ spc () ++ - pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++ + prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ + pr_with_names ids ++ pr_opt (pr_eliminator env) e) | TacDoubleInduction (h1,h2) -> hov 1 |