aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/interactive
Commit message (Collapse)AuthorAge
* Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
|
* Error box detection run only on errorGravatar Enrico Tassi2016-06-06
| | | | | Advantage: 0 cost if no error occurs Disadvantage: a box *must* end with the error absorbing command
* STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
|
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* Test file for bug #4289 (buggy hash-consing of kernel name pairsGravatar Hugo Herbelin2015-07-30
| | | | | | breaking backtracking in the presence of functors). In "interactive" rather than "bugs" because of the use of Back.
* nanoPG: better copy/pasteGravatar Enrico Tassi2014-03-13
|
* rename Paral-ITP demo fileGravatar Enrico Tassi2014-01-13
|
* Paral-ITP demo: better commentsGravatar Enrico Tassi2014-01-13
|
* STM: fix very simple demoGravatar Enrico Tassi2014-01-13
|
* fix simple test for paral-itpGravatar Enrico Tassi2014-01-06
|
* demo file for paral-itpGravatar gareuselesinge2013-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16832 85f007b7-540e-0410-9357-904b9bb8a0f7
* Trickyer test for Paral-ITPGravatar gareuselesinge2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
| | | | | | | | | | | | | | | Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test for Paral-ITPGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1229 (toplevel "unresolved evar" fled throughGravatar herbelin2006-09-23
| | | | | | | Declare Implicit Tactic support) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interactive test of BackGravatar herbelin2005-11-01
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7486 85f007b7-540e-0410-9357-904b9bb8a0f7