aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/test/ListDep.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-06-17Cleanup in subtac_cases, preparing to use improvements on return predicatemsozeau
inference. Little improvement un subtac_obligations: do not retry to solve all obligations when finishing to solve one obligation nobody depends on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11133 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-26Make multiple patterns work again with Program while simplifying the code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9732 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-13Solve obligation handling bug of trying to solve automatically at Next ↵msozeau
Obligation time. Now done at Qed or Defined. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9700 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-23Debug wellfounded defs, work on cleaning obls envsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9674 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28Add dependent list combinators test.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9184 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 21:16:08 +0000