diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 2 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index f5be5cb30..335afddd2 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -671,7 +671,7 @@ and ct_TACTIC_COM = | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES | CT_move_after of ct_ID * ct_ID | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT - | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT + | CT_new_induction of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT | CT_omega | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 9e00aed3b..88852aa59 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1665,7 +1665,7 @@ and fTACTIC_COM = function fINTRO_PATT_OPT x3; fNODE "new_destruct" 3 | CT_new_induction(x1, x2, x3) -> - fFORMULA_OR_INT x1; + (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *) fUSING x2; fINTRO_PATT_OPT x3; fNODE "new_induction" 3 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index f17cb67b4..323d885a2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1161,8 +1161,8 @@ and xlate_tac = (xlate_int_or_constr a, xlate_using b, xlate_with_names c) | TacNewInduction(a,b,c) -> - CT_new_induction - (xlate_int_or_constr a, xlate_using b, + CT_new_induction (* Pierre C. : est-ce correct *) + (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) (*| TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, |