| Age | Commit message (Expand) | Author |
|---|
| 2017-06-15 | Merge PR#713: Bump year in headers. | Maxime Dénès |
| 2017-06-15 | Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints | Maxime Dénès |
| 2017-06-15 | Merge PR#752: Adding a test case as requested in bug 5205. | Maxime Dénès |
| 2017-06-15 | Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports | Maxime Dénès |
| 2017-06-09 | Fix Bug #5568, no dup notation warnings on repeated module imports | Paul Steckler |
| 2017-06-08 | Adding a test case as requested in bug 5205. | Théo Zimmermann |
| 2017-06-05 | Univs: fix bug #5365, generation of u+k <= v constraints | Matthieu Sozeau |
| 2017-06-02 | Merge PR#705: Fix bug #5019 (looping zify on dependent types) | Maxime Dénès |
| 2017-06-01 | Merge PR#631: Fix bug #5255 | Maxime Dénès |
| 2017-06-01 | Bump year in headers. | Maxime Dénès |
| 2017-06-01 | Fix bug #5019 (looping zify on dependent types) | Jason Gross |
| 2017-06-01 | Add opened bug 5019 | Jason Gross |
| 2017-06-01 | Merge PR#710: Add test-suite checks for coqchk with constraints | Maxime Dénès |
| 2017-05-31 | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (... | Maxime Dénès |
| 2017-05-31 | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti... | Maxime Dénès |
| 2017-05-30 | Add test-suite checks for coqchk with constraints | Jason Gross |
| 2017-05-30 | Merge PR#693: A subtle bug in tclWITHHOLES. | Maxime Dénès |
| 2017-05-30 | Fix bug 5550: "typeclasses eauto with" does not work with section variables. | Théo Zimmermann |
| 2017-05-29 | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey |
| 2017-05-29 | Merge PR#546: Fix for bug #4499 and other minor related bugs | Maxime Dénès |
| 2017-05-28 | Fixing a subtle bug in tclWITHHOLES. | Hugo Herbelin |
| 2017-05-28 | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès |
| 2017-05-26 | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin... | Maxime Dénès |
| 2017-05-25 | Bug 5546, qualify datatype constructors when needed | Paul Steckler |
| 2017-05-20 | Merge PR#653: Bug #5535, test for Show with -emacs | Maxime Dénès |
| 2017-05-19 | add test for Show with -emacs, bug 5535 | Paul Steckler |
| 2017-05-17 | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler |
| 2017-05-17 | fix swapping of ids in tuples, bug 5486 | Paul Steckler |
| 2017-05-16 | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters). | Hugo Herbelin |
| 2017-05-16 | Fixing a bug with nested "as" clauses in "match". | Hugo Herbelin |
| 2017-05-15 | Fix #5255: [Context (x : T := y)] should mean [Let x := y]. | Pierre-Marie Pédrot |
| 2017-05-03 | FIx bug #5300: uncaught exception in "Print Assumptions". | Cyprien Mangin |
| 2017-05-02 | Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with... | Maxime Dénès |
| 2017-05-02 | Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files | Maxime Dénès |
| 2017-05-01 | Fixing Set Rewriting Schemes bugs introduced in v8.5. | Hugo Herbelin |
| 2017-05-01 | remove unneeded -emacs flag to coq-prog-args | Paul Steckler |
| 2017-05-01 | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | Hugo Herbelin |
| 2017-05-01 | Really fixing #2602 which was wrongly working because of #5487 hiding the cause. | Hugo Herbelin |
| 2017-04-28 | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)." | Maxime Dénès |
| 2017-04-28 | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | Hugo Herbelin |
| 2017-04-27 | Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx. | Pierre-Marie Pédrot |
| 2017-04-20 | Fix bug #5377: @? patterns broken. | Pierre-Marie Pédrot |
| 2017-04-19 | Merge PR#538: Correction of bug #4306 | Maxime Dénès |
| 2017-04-14 | Fixing bug #5470 (anomaly on notations with misused "binder" type). | Hugo Herbelin |
| 2017-04-14 | Fixing bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin |
| 2017-04-14 | Fix anomaly when doing [all:Check _.] during a proof. | Gaetan Gilbert |
| 2017-04-13 | Reinstate fixpoint refolding in [cbn], deactivated by mistake. | Matthieu Sozeau |
| 2017-04-08 | Fixing #5460 (limitation in computing deps in pattern-matching compilation). | Hugo Herbelin |
| 2017-04-07 | Better support for printing constructors with let-ins. | Hugo Herbelin |
| 2017-04-07 | Fixing #4499 (not using unnamed record field in {| |} notation). | Hugo Herbelin |
