diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 6 |
3 files changed, 7 insertions, 5 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 94d185211..9bb8d0754 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -357,8 +357,8 @@ GEXTEND Gram (* Derived basic tactics *) | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> TacSimpleInduction h - | IDENT "induction"; c = induction_arg; ids = with_names; - el = OPT eliminator -> TacNewInduction (c,el,ids) + | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; + el = OPT eliminator -> TacNewInduction (lc,el,ids) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8e8413de4..9ec4dfd03 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -685,7 +685,7 @@ and pr_atom1 env = function hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) | TacNewInduction (h,e,ids) -> hov 1 (str "induction" ++ spc () ++ - pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++ + prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ pr_opt (pr_eliminator env) e) | TacSimpleDestruct h -> hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6d27c274c..f33c5a955 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -319,10 +319,12 @@ let rec mlexpr_of_atomic_tactic = function (* Derived basic tactics *) | Tacexpr.TacSimpleInduction h -> <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >> - | Tacexpr.TacNewInduction (c,cbo,ids) -> + | Tacexpr.TacNewInduction (cl,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> +(* let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in *) +(* <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> *) + <:expr< Tacexpr.TacNewInduction $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>> | Tacexpr.TacSimpleDestruct h -> <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacNewDestruct (c,cbo,ids) -> |