aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Fixing #5277 (Scheme Equality not robust wrt choice of names).Gravatar Hugo Herbelin2016-12-22
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\
| * Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
| |\
| * | Comment on universe handling in ParametersGravatar Matthieu Sozeau2016-12-02
| * | Univs: fix bug #5188Gravatar Matthieu Sozeau2016-12-02
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\| |
| | * Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
| |/
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| * Stop parsing -compat-notations options, which are no longer supported (bug #3...Gravatar Guillaume Melquiond2016-11-21
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| * Fix bug in warnings: -w foo was silent when foo did not exist.Gravatar Maxime Dénès2016-11-14
| * Do not mention "none" in warnings doc, as it is there for compatibility.Gravatar Maxime Dénès2016-11-14
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
| | * Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
| * | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \
| * | | Improve formatting of a message in [Arguments].Gravatar Maxime Dénès2016-11-07
| * | | Fix #5181: [Arguments] no longer correctly checks the length of arguments listsGravatar Maxime Dénès2016-11-07
| * | | Fix #5182: "Arguments names must be distinct." is bogus and underinformativeGravatar Maxime Dénès2016-11-07
| * | | Not using style tags when translating/beautifying a file.Gravatar Hugo Herbelin2016-11-05
| * | | Quick fix of tactic parsing while Load-ing in coqide.Gravatar Hugo Herbelin2016-11-04
| * | | Add documentation for [Set Warnings] and the -w option.Gravatar Cyprien Mangin2016-11-04
| | | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| * | | Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
* | | | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | |
| * | | Removing dead code.Gravatar Hugo Herbelin2016-10-29
| | |/ | |/|
| * | Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \
| * \ \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \
| | * | | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| * | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\ \ \ \
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | | | |
| | | | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |_|_|/ | |/| | |
| | * | | Fix a bug in error printing of unif constraintsGravatar Matthieu Sozeau2016-10-22
| * | | | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| | | | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| | |_|/ | |/| |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\| | |
| * | | [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
| * | | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
| * | | Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
| * | | Grouping checks about commands together.Gravatar Hugo Herbelin2016-10-17
| * | | Vernac.ml: parenthesizing a side-effect.Gravatar Hugo Herbelin2016-10-17
| * | | Factorizing two instances of load_vernac.Gravatar Hugo Herbelin2016-10-17
| * | | Passing chan_beautify functionally rather than by side-effect.Gravatar Hugo Herbelin2016-10-17
| * | | Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
| * | | More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
| * | | Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\| | |
| * | | Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Gravatar Pierre-Marie Pédrot2016-10-16
| | |/ | |/|