aboutsummaryrefslogtreecommitdiff
path: root/test-suite/interactive
AgeCommit message (Expand)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-06-11[test-suite] [stm] Interactive test case for fail-on-qed.Emilio Jesus Gallego Arias
2019-05-23Fixing typos - Part 3JPR
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31WIP: adapt Numeral Notation to synchronized prim notationsPierre Letouzey
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2016-06-06Error box detection run only on errorEnrico Tassi
2016-06-06STM: proof block detection made optional + simple testEnrico Tassi
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-07-30Test file for bug #4289 (buggy hash-consing of kernel name pairsHugo Herbelin
2014-03-13nanoPG: better copy/pasteEnrico Tassi
2014-01-13rename Paral-ITP demo fileEnrico Tassi
2014-01-13Paral-ITP demo: better commentsEnrico Tassi
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-06fix simple test for paral-itpEnrico Tassi
2013-10-01demo file for paral-itpgareuselesinge
2013-08-30Trickyer test for Paral-ITPgareuselesinge
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-08Test for Paral-ITPgareuselesinge
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2006-09-23Correction bug #1229 (toplevel "unresolved evar" fled throughherbelin
2005-11-01Interactive test of Backherbelin