aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
* Adding a test case as requested in bug 5205.Gravatar Théo Zimmermann2017-06-08
* Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
|\
* \ Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
|\ \
| | * Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | * Add opened bug 5019Gravatar Jason Gross2017-06-01
| |/ |/|
* | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Gravatar Maxime Dénès2017-05-31
|\ \
| * | Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
* | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
|/ /
* | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin...Gravatar Maxime Dénès2017-05-26
|\ \
| * | Fixing bug #5526,allow nonlinear variables in Notation patternsGravatar Paul Steckler2017-05-17
* | | fix swapping of ids in tuples, bug 5486Gravatar Paul Steckler2017-05-17
* | | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
|/ /
| * Fix #5255: [Context (x : T := y)] should mean [Let x := y].Gravatar Pierre-Marie Pédrot2017-05-15
|/
* FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
* Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...Gravatar Maxime Dénès2017-05-02
|\
* \ Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesGravatar Maxime Dénès2017-05-02
|\ \
| * | remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| | * Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-05-01
| |/ |/|
* | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Gravatar Maxime Dénès2017-04-28
|/
* Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-04-28
* Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Gravatar Pierre-Marie Pédrot2017-04-27
* Fix bug #5377: @? patterns broken.Gravatar Pierre-Marie Pédrot2017-04-20
* Merge PR#538: Correction of bug #4306Gravatar Maxime Dénès2017-04-19
|\
* | Fixing bug #5470 (anomaly on notations with misused "binder" type).Gravatar Hugo Herbelin2017-04-14
* | Fixing bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-04-14
* | Fixing #5460 (limitation in computing deps in pattern-matching compilation).Gravatar Hugo Herbelin2017-04-08
| * closing bug file for #4306Gravatar Julien Forest2017-04-04
| * bug file for 4306Gravatar Julien Forest2017-04-04
* | Test file for #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
|/
* Add test file for #4957.Gravatar Maxime Dénès2017-04-03
* Merge PR#507: Intern names bound in match patternsGravatar Maxime Dénès2017-03-23
|\
| * Intern names bound in match patternsGravatar Tej Chajed2017-03-23
* | funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
|/
* Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc...Gravatar Maxime Dénès2017-03-10
|\
* | Fixing bug #5346 (an unimplemented application of 'pat).Gravatar Hugo Herbelin2017-02-09
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
|\ \
| * | Fixing #5311 (anomaly on unexpected intro pattern).Gravatar Hugo Herbelin2017-01-31
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
|\| |
| * | Fixing unification regression #5323.Gravatar Hugo Herbelin2017-01-23
* | | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Gravatar Hugo Herbelin2017-01-22
* | | Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
|\ \ \
* \ \ \ Merge remote-tracking branch 'github/pr/378' into v8.6Gravatar Maxime Dénès2016-12-04
|\ \ \ \
| * | | | Univs: fix bug #5188Gravatar Matthieu Sozeau2016-12-02
* | | | | Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
|/ / / /
| * / / Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
|/ / /
* | | Merge commit '633ed9c' into v8.6Gravatar Maxime Dénès2016-11-17
|\ \ \
| * | | Add test suite files for 4700-4785Gravatar Jason Gross2016-11-17
* | | | Revert more of a477dc for good measureGravatar Matthieu Sozeau2016-11-16
* | | | Revert part of a477dc, disallow_shelvedGravatar Matthieu Sozeau2016-11-15
* | | | Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
|\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 04:35:40 +0000