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 | |
| 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')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 3 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9bb8d07541..e8829acbab 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -363,8 +363,8 @@ GEXTEND Gram h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis -> TacSimpleDestruct h - | IDENT "destruct"; c = induction_arg; ids = with_names; - el = OPT eliminator -> TacNewDestruct (c,el,ids) + | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; + el = OPT eliminator -> TacNewDestruct (lc,el,ids) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr 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 diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index f33c5a9559..b05895666f 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -330,7 +330,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacNewDestruct (c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >> + <:expr< Tacexpr.TacNewDestruct $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> |