aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* fix test-suite/coq-makefile/findlib-package on windowsGravatar Enrico Tassi2017-09-04
* Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsGravatar Maxime Dénès2017-08-31
|\
* \ Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateGravatar Maxime Dénès2017-08-31
|\ \
* \ \ Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagGravatar Maxime Dénès2017-08-31
|\ \ \
* \ \ \ Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \ \ \
* \ \ \ \ Merge PR #998: Avoid running interactive tests on Windows.Gravatar Maxime Dénès2017-08-30
|\ \ \ \ \
| | * | | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsGravatar Enrico Tassi2017-08-29
| * | | | | Avoid running interactive tests on Windows.Gravatar Maxime Dénès2017-08-29
| | | | | * Properly handling parameters of primitive projections in cctac.Gravatar Pierre-Marie Pédrot2017-08-29
| | | | | * Fix BZ#5697: Congruence does not work with primitive projections.Gravatar Pierre-Marie Pédrot2017-08-29
| |_|_|_|/ |/| | | |
* | | | | Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \
* \ \ \ \ \ Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | | | |
| | | | * | | coq_makefile: use dedicated variable for extra packagesGravatar Enrico Tassi2017-08-29
| | | | * | | coq_makefile: test using findlib's packageGravatar Enrico Tassi2017-08-29
| |_|_|/ / / |/| | | | |
| | | * | | Adding a test for #5569 (warning about skipping spaces).Gravatar Hugo Herbelin2017-08-29
| | | * | | Dropping former fix to bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-08-29
| | | * | | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| | | | * | primproj: fix bug 5245, hnf on proj with simpl never flag.Gravatar Matthieu Sozeau2017-08-25
| | | |/ /
| | | | * Program: fix BZ#5683, missing lift when building case predicateGravatar Matthieu Sozeau2017-08-24
| | | |/
* | | / Fix coqdoc test-suite target on Windows.Gravatar Théo Zimmermann2017-08-21
| |_|/ |/| |
* | | Merge PR #942: solving b1859Gravatar Maxime Dénès2017-08-16
|\ \ \
* \ \ \ Merge PR #954: Print names of all open blocksGravatar Maxime Dénès2017-08-16
|\ \ \ \
* \ \ \ \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \ \ \
* \ \ \ \ \ Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \
| | | | | * | | Adding a test for BZ#1859 as suggested by @tchajed.Gravatar Théo Zimmermann2017-08-15
| | | | * | | | Print names of all open blocksGravatar Tej Chajed2017-08-06
| |_|_|/ / / / |/| | | | | |
| | | | | * | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #926: test-suite uses Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \
| | | | | * | | | | Change the option for cumulativityGravatar Amin Timany2017-07-31
| | | | | * | | | | Add Jason's example of fun-ext with cumulativityGravatar Amin Timany2017-07-31
| | | | | * | | | | Add test for NonCumulative inductivesGravatar Amin Timany2017-07-31
| | | | | * | | | | Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
| | | | | | |_|/ / | | | | | |/| | |
* | | | | / | | | closing bug 5315Gravatar Julien Forest2017-07-29
| |_|_|_|/ / / / |/| | | | | | |
| | | | * | | | Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| |_|_|/ / / / |/| | | | | |
| | | * | | | test-suite: more use of the new command Extraction TestCompileGravatar Pierre Letouzey2017-07-27
* | | | | | | Fix TypeclassDebug.out after conflicting PR mergesGravatar Matthieu Sozeau2017-07-26
| | | * | | | test-suite/success/extraction.v : add some Extraction TestCompileGravatar Pierre Letouzey2017-07-26
| | | * | | | Enrich test file 4720.v with a compilation test of the extracted codeGravatar Pierre Letouzey2017-07-26
| |_|/ / / / |/| | | | |
| | * | | | adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...Gravatar Pierre Letouzey2017-07-26
| |/ / / / |/| | | |
* | | | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \
| | * | | | Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
| |/ / / / |/| | | |
* | | | | Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\ \ \ \ \
| | * | | | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Gravatar Pierre Letouzey2017-07-25
| |/ / / / |/| | | |
| * | | | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
* | | | | fake_ide: do as coqide to find out coqtop pathGravatar Enrico Tassi2017-07-20