aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2083.v
AgeCommit message (Collapse)Author
2013-09-20Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19Fix bugs related to Program integration.msozeau
- reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
changes in obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12514 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
{measure ms [id] [(rel)]}. Fix script of bug #2083 and test-suite file accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12032 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Fixes in Program well-founded definitions:msozeau
- de Bruijn bug #2083 - Avoid useless eta-expansion (bug #2060) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12020 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 21:05:25 +0000