diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-10 18:34:51 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-10 18:34:51 +0000 |
| commit | 94d27c5f40b55b06142443e8ae0b28c4432c090e (patch) | |
| tree | bf4196b721d9854cc203b6b96214a236e5b81b3c /parsing/pptactic.ml | |
| 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 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |