From 94d27c5f40b55b06142443e8ae0b28c4432c090e Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 10 Feb 2006 18:34:51 +0000 Subject: 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 --- proofs/clenvtac.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'proofs/clenvtac.ml') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 6a0ea6096..8bba76007 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 -- cgit v1.2.3