diff options
| author | coq | 2006-02-10 18:34:51 +0000 |
|---|---|---|
| committer | coq | 2006-02-10 18:34:51 +0000 |
| commit | 94d27c5f40b55b06142443e8ae0b28c4432c090e (patch) | |
| tree | bf4196b721d9854cc203b6b96214a236e5b81b3c /contrib/interface | |
| parent | 5384ed9ab7557c515c8522b0229f10663e5a3161 (diff) | |
induction now admits multiple induction arguments. The principle must
be explicitely given, and ALL parameters and args of the scheme must
be given (only branches must be omitted). For the moment, only
principle like generated by GenFixpoint (functional induction) are
usable. That is the predicate must have a additional paramter like in:
(P x1 ... xn (f p1...pm x1...xn))
Example of use : induction x y (add x y) using add_ind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
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 f5be5cb306..335afddd22 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 9e00aed3b9..88852aa59c 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 f17cb67b43..323d885a27 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, |