aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Maxime Dénès
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29Adding a test for #5569 (warning about skipping spaces).Hugo Herbelin
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-21Fix coqdoc test-suite target on Windows.Théo Zimmermann
2017-08-16Merge PR #942: solving b1859Maxime Dénès
2017-08-16Merge PR #954: Print names of all open blocksMaxime Dénès
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-08-16Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...Maxime Dénès
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-15Adding a test for BZ#1859 as suggested by @tchajed.Théo Zimmermann
2017-08-06Print names of all open blocksTej Chajed
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Maxime Dénès
2017-08-01Merge PR #926: test-suite uses Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-08-01Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Maxime Dénès
2017-07-31Change the option for cumulativityAmin Timany
2017-07-31Add Jason's example of fun-ext with cumulativityAmin Timany
2017-07-31Add test for NonCumulative inductivesAmin Timany
2017-07-31Issue error on monomorphic cumulative inductivesAmin Timany
2017-07-29closing bug 5315Julien Forest
2017-07-27Fixing bug #5671 (specialize unclean wrt Metas).Hugo Herbelin
2017-07-27test-suite: more use of the new command Extraction TestCompilePierre Letouzey
2017-07-26Fix TypeclassDebug.out after conflicting PR mergesMatthieu Sozeau
2017-07-26test-suite/success/extraction.v : add some Extraction TestCompilePierre Letouzey
2017-07-26Enrich test file 4720.v with a compilation test of the extracted codePierre Letouzey
2017-07-26adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...Pierre Letouzey
2017-07-26Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Maxime Dénès
2017-07-26Adding support for recursive notations of the form "x , .. , y , z".Hugo Herbelin
2017-07-26Merge PR #857: Extraction: various fixes related with bug 4720Maxime Dénès
2017-07-25Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Pierre Letouzey
2017-07-20Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Pierre Letouzey
2017-07-20fake_ide: do as coqide to find out coqtop pathEnrico Tassi
2017-07-20more verbose logs for coq-makefileEnrico Tassi
2017-07-20coq-makefile: make test suite detect more errorsEnrico Tassi
2017-07-20Remove trailing CR before diff in output and misc tests.Maxime Dénès
2017-07-20Print failure logs on appveyor.Maxime Dénès
2017-07-20Remove non-terminating Timeout tests from Hints.v.Maxime Dénès
2017-07-20Make coqlib relative in test suite (revert 024a7ab20b0)Maxime Dénès
2017-07-20Merge PR #869: Enforce alternating separators in typeclass debug outputMaxime Dénès
2017-07-20Merge branch 'v8.7'Maxime Dénès
2017-07-19Removing testing unsupported Next.Hugo Herbelin
2017-07-19Merge PR #745: Add timing scriptsMaxime Dénès
2017-07-17Adding a coqdoc target to test-suite.Hugo Herbelin
2017-07-14Getting rid of abstraction breaking code in tclABSTRACT.Pierre-Marie Pédrot
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
2017-07-13Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:23:28 +0000