aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/test/Mutind.v
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
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
2007-08-26Fix de Bruijn bug in wf definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Various fixes in subtac, update some test cases.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9553 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Work on mutual defs, various bug fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9360 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Mutually structurally recursive defs and rec using measures added.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8968 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14Test files for subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8714 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 07:52:12 +0000