| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | * | | | | | | | | Adding a primitive to recover the set of keywords from the lexer. |  Pierre-Marie Pédrot | 2016-10-21 | |
| | | * | | | | | | | Revert "unification.ml: fix for bug #4763, unif regression" |  Maxime Dénès | 2016-10-21 | |
| | | | | | | | | * | sections/hints: prevent Not_found in get_type_of |  Matthieu Sozeau | 2016-10-21 | |
| | | |_|_|_|_|_|/ | |/| | | | | | | ||||
| | * | | | | | | | Merge branch 'fixminimization' into v8.6 | Matthieu Sozeau | 2016-10-21 | |
| | |\ \ \ \ \ \ \ | ||||
| | * | | | | | | | | Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3 | Matthieu Sozeau | 2016-10-21 | |
| | | * | | | | | | | Remove no longer exported debug printer | Matthieu Sozeau | 2016-10-21 | |
| | | | * | | | | | | Merge remote-tracking branch 'github/pr/328' into v8.5 | Maxime Dénès | 2016-10-21 | |
| | | | |\ \ \ \ \ \ | ||||
| | * | | \ \ \ \ \ \ | Merge remote-tracking branch 'github/pr/233' into v8.6 | Maxime Dénès | 2016-10-21 | |
| | |\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | Adding dependency of the test-suite subsystems in prerequisite (fixing #5150). |  Hugo Herbelin | 2016-10-20 | |
| | | | | * | | | | | | | A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars). | Hugo Herbelin | 2016-10-20 | |
| | | | * | | | | | | | | Cleanup code according to comments. | Matthieu Sozeau | 2016-10-20 | |
| | | | * | | | | | | | | Fix minimization to be insensitive to redundant arcs. | Matthieu Sozeau | 2016-10-20 | |
| | | |/ / / / / / / / | |/| | | | | | | | | ||||
| | * | | | | | | | | | Merge branch 'bug5036' into v8.6 | Matthieu Sozeau | 2016-10-20 | |
| | |\ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | Fix bug #5036 autorewrite, sections and universes | Matthieu Sozeau | 2016-10-20 | |
| | | | * | | | | | | | | [search] Don't build intermediate lists in search. |  Emilio Jesus Gallego Arias | 2016-10-20 | |
| | | |/ / / / / / / / | |/| | | | | | | | | ||||
| * | | | | | | | | | | COMMENTS: dev/doc/changes.txt |  Matej Kosik | 2016-10-20 | |
| * | | | | | | | | | | CLEANUP: Namegen.to_avoid | Matej Kosik | 2016-10-20 | |
| | * | | | | | | | | | Merge remote-tracking branch 'github/printcandidates' into v8.6 | Matthieu Sozeau | 2016-10-20 | |
| | |\ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | Refine printing of pending unification constraints | Matthieu Sozeau | 2016-10-20 | |
| | |/ / / / / / / / / | ||||
| | | | | | | * | | | | Documenting Hint Resolve -> and <- variants. |  Théo Zimmermann | 2016-10-19 | |
| | * | | | | | | | | | Test for variant of #5142 (good error message on pattern-matching failure). | Hugo Herbelin | 2016-10-19 | |
| | * | | | | | | | | | Attempt to improve error rendering in pattern-matching compilation (#5142). | Hugo Herbelin | 2016-10-19 | |
| * | | | | | | | | | | enriching ".gitignore" | Matej Kosik | 2016-10-19 | |
| | * | | | | | | | | | More comments in VM. | Maxime Dénès | 2016-10-19 | |
| | * | | | | | | | | | Error Resiliency: more conservative default (only curly braces) |  Enrico Tassi | 2016-10-19 | |
| | | | | | | * | | | | Making the doc of auto hints more precise. | Théo Zimmermann | 2016-10-19 | |
| * | | | | | | | | | | COMMENT: was added to "Nameops.increment_suffix". | Matej Kosik | 2016-10-19 | |
| * | | | | | | | | | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript". | Matej Kosik | 2016-10-19 | |
| * | | | | | | | | | | Converting certain "order-only" (Makefile) dependencies to regular dependencies. | Matej Kosik | 2016-10-19 | |
| | | | | * | | | | | | Change the order of arguments of fig2dev. | Théo Zimmermann | 2016-10-19 | |
| | | | |/ / / / / / | ||||
| | | | | | | | | * | [pp] Use more convenient pp API in ssrmatching | Emilio Jesus Gallego Arias | 2016-10-18 | |
| | | | | | | | | * | [pp] Try to properly tag error messages in cError. | Emilio Jesus Gallego Arias | 2016-10-18 | |
| | | | | | | | | * | [pp] Add tagging function to all low-level printing calls. | Emilio Jesus Gallego Arias | 2016-10-18 | |
| * | | | | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-18 | |
| |\ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|/ | |/| | | | | | | | ||||
| | | | | | | * | | | Extending the doc with a general summary of auto variants. | Théo Zimmermann | 2016-10-18 | |
| | | | | | | * | | | Document info_auto. | Théo Zimmermann | 2016-10-18 | |
| | | * | | | | | | | [stm] Fix record field name clash. | Emilio Jesus Gallego Arias | 2016-10-18 | |
| | |/ / / / / / / | ||||
| | | | | | * / / | Improve the documentation of eauto. |  Théo Zimmermann | 2016-10-18 | |
| | | | | |/ / / | | | |/| | | | ||||
| | * | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-18 | |
| | |\ \ \ \ \ \ | | | |/ / / / | | |/| | | | | ||||
| | | * | | | | | Removing output test for module qualification. | Pierre-Marie Pédrot | 2016-10-18 | |
| | * | | | | | | Quick fix to unification regression #4955. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Extra warning about unicode character of unknown status following an ident. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Fixing a few other inconsistencies with notations. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Stopping warning on unrecognized unicode character in notation (fixing #5136). | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | [toplevel] Remove undocumented "just_parsing" flag. | Emilio Jesus Gallego Arias | 2016-10-17 | |
| | * | | | | | | [toplevel] Remove duplicate beautify flags. | Emilio Jesus Gallego Arias | 2016-10-17 | |
| | * | | | | | | Vernac.ml: inlining read_vernac_file within load_vernac. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Grouping checks about commands together. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Vernac.ml: parenthesizing a side-effect. | Hugo Herbelin | 2016-10-17 | |
| | * | | | | | | Factorizing two instances of load_vernac. | Hugo Herbelin | 2016-10-17 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |