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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 6a0ea6096b..8bba760074 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -66,6 +66,7 @@ let clenv_refine clenv gls = (refine (clenv_cast_meta clenv (clenv_value clenv))) gls + let res_pf clenv ?(allow_K=false) gls = clenv_refine (clenv_unique_resolver allow_K clenv gls) gls diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index c487c34a05..42a5d5cbe2 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -138,7 +138,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis - | TacNewInduction of 'constr induction_arg * 'constr with_bindings option + | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option * intro_pattern_expr | TacSimpleDestruct of quantified_hypothesis | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option |