diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 16:42:26 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 16:42:26 +0000 |
| commit | c164dc2aadd8d26b362669b9af6b45cbd8e563ff (patch) | |
| tree | beb528d5a47d69ef81c52f9ddbef17cde7fb9e26 /doc/refman/Program.tex | |
| parent | 14eb998277c1639a02139023a642ee680f6c6a79 (diff) | |
Backport code from command.ml to subtac_command.ml for definining
recursive definitions. Now program accepts cofixpoints and uses the new
way infer structurally decreasing arguments. Also, checks for correct
recursive calls before giving the definition to the obligations machine
(solves part 1 of bug #1784).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/Program.tex')
0 files changed, 0 insertions, 0 deletions