aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Add fixed test-suite file for bug #4527Gravatar Matthieu Sozeau2016-09-27
* Unbreak Ltac [ | .. | ] notation in -compat 8.5Gravatar Jason Gross2016-09-26
* Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
* Posssible abstractions over goal variables when inferring match return clause.Gravatar Hugo Herbelin2016-09-26
* Trying an abstracting dependencies heuristic for the match return clause even...Gravatar Hugo Herbelin2016-09-26
* Trying a no-inversion no-dependency heuristic for match return clause.Gravatar Hugo Herbelin2016-09-26
* Fix bug #5093: typeclasses eauto depth arg does not accept a var.Gravatar Pierre-Marie Pédrot2016-09-26
* Adding a test for bug #5096.Gravatar Pierre-Marie Pédrot2016-09-24
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-23
|\
| * Fixing #5095 (non relevant too strict test in let-in abstraction).Gravatar Hugo Herbelin2016-09-22
* | Further "decide equality" tests on demand of Jason.Gravatar Hugo Herbelin2016-09-17
* | Added a test file for contradiction.Gravatar Hugo Herbelin2016-09-15
* | Continuing fix to #5078, taking also into account intropatterns.Gravatar Hugo Herbelin2016-09-15
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * Fixing test-suite after commit 43104a0b.Gravatar Pierre-Marie Pédrot2016-09-14
* | test-suite/output-modulo-time made more robustGravatar Enrico Tassi2016-09-13
| * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
* | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
|\ \
* | | Add support for testing output mod timing changesGravatar Jason Gross2016-09-11
* | | Add a test for 4836Gravatar Jason Gross2016-09-11
| | * Test for #5077.Gravatar Hugo Herbelin2016-09-10
| * | no-refold patchGravatar Paul Steckler2016-09-09
* | | Fix output test-suite after commit 0d3c319.Gravatar Pierre-Marie Pédrot2016-09-09
|/ /
* | Update csdp cache.Gravatar Pierre-Marie Pédrot2016-09-09
* | Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
* | Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-07
|\|
* | micromega : more robust generation of proof termsGravatar Frédéric Besson2016-09-07
| * Test file for #5065 - Anomaly: Not a proof by inductionGravatar Maxime Dénès2016-09-05
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
|\|
| * Fix test-suite after Frédéric's 6231f07b2.Gravatar Maxime Dénès2016-09-01
* | Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Gravatar Frédéric Besson2016-08-31
| * Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
* | Fixing output test-suite after warning for inner Requires.Gravatar Pierre-Marie Pédrot2016-08-30
* | Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-08-30
* | plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...Gravatar Frédéric Besson2016-08-30
* | Fix bug #3920: eapply masks an hypothesis name.Gravatar Pierre-Marie Pédrot2016-08-30
* | Fix bug #4764: Syntactic notation externalization breaks.Gravatar Pierre-Marie Pédrot2016-08-28
* | Fix bug #4904: [Import] does not load intermediately unqualified names of ali...Gravatar Pierre-Marie Pédrot2016-08-23
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\|
| * Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
* | Test file for bug #4187.Gravatar Pierre-Marie Pédrot2016-08-19
* | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
|\ \
* | | Adding a test for bug #4653.Gravatar Pierre-Marie Pédrot2016-08-18
* | | Fixing #3070 ("subst" taking properly into account chains of dependencies).Gravatar Hugo Herbelin2016-08-17
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\ \ \ | | |/ | |/|
| * | Fix bug #4673: regression in setoid_rewrite.Gravatar Matthieu Sozeau2016-07-29
* | | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\| |
| * | Fix bug #3886, generation of obligations of fixesGravatar Matthieu Sozeau2016-07-29
| * | Fix #4769, univ poly and elim schemes in sectionsGravatar Matthieu Sozeau2016-07-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 16:13:11 +0000