diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-01 14:23:47 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-01 14:23:47 +0000 |
| commit | 98ebcece4ff6d2d9450dc96206b271516167daa5 (patch) | |
| tree | dfcb37805cc13d7573ed48aa83bd7f9037ada0d1 /ide/config_lexer.mll | |
| parent | 1ca3746894032d4372d7937b6b4188f8c4996c35 (diff) | |
Added some tests to make more robust the tactique "Functional
Induction". Namely: check that the given function is a really a
constant, and check that the number of given argument is exactly the
arity of the given function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3723 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/config_lexer.mll')
0 files changed, 0 insertions, 0 deletions