Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | | * | | | | | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | 2017-05-16 | |
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | ||||
| | | | | | | * | | | | | Simplified compaction criterion + tests. | Pierre Courtieu | 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-16 | |
| | | | * | | | | | | | | Merge PR#624: Switch bedrock to mit-plv base | Maxime Dénès | 2017-05-16 | |
| | | | |\ \ \ \ \ \ \ \ | | | | | |/ / / / / / / | | | | |/| | | | | | | | ||||
* | | | | | | | | | | | | Merge PR#626: Add documentation for Set Ltac Batch Debug | Maxime Dénès | 2017-05-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#629: A couple of simple updates for Travis | Maxime Dénès | 2017-05-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | | | Dead code in coqdep. | Hugo Herbelin | 2017-05-15 | |
| | | | * | | | | | | | | | | [interp] Rework check for casts inside patterns. | Emilio Jesus Gallego Arias | 2017-05-15 | |
| | | | * | | | | | | | | | | [interp] [ast] Make raw_cases_pattern_expr private. | Emilio Jesus Gallego Arias | 2017-05-15 | |
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | Typo in comments of constrintern. | Hugo Herbelin | 2017-05-15 | |
| | | | | * | | | | | | | | Removing a line warned unused. | Hugo Herbelin | 2017-05-14 | |
| | | | | * | | | | | | | | Removing a variable warned unused. | Hugo Herbelin | 2017-05-14 | |
| * | | | | | | | | | | | | [travis] Update OCaml to 4.04.1 | Emilio Jesus Gallego Arias | 2017-05-13 | |
| * | | | | | | | | | | | | [travis] Move VST to required suite. | Emilio Jesus Gallego Arias | 2017-05-13 | |
|/ / / / / / / / / / / / | ||||
| | * | | | | | | | | | | Uniformity of style for selecting plural or not; spacing for comma. | Hugo Herbelin | 2017-05-13 | |
| | * | | | | | | | | | | Typo in a comment of plugin Quote. | Hugo Herbelin | 2017-05-13 | |
| | * | | | | | | | | | | Aligning on standard layout of CHANGES. | Hugo Herbelin | 2017-05-13 | |
| |/ / / / / / / / / / |/| | | | | | | | | | | ||||
| * | | | | | | | | | | Add documentation for Set Ltac Batch Debug | Jason Gross | 2017-05-11 | |
|/ / / / / / / / / / | ||||
| | | | | * | | | | | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu | 2017-05-11 | |
| | | | | | * | | | | Obligations shrinking: shrink abstraction too | Matthieu Sozeau | 2017-05-11 | |
| |_|_|_|_|/ / / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR#594: An example showing the benefit of Econstr | Maxime Dénès | 2017-05-11 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a... | Maxime Dénès | 2017-05-11 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#572: Replacing costly merges in UGraph. | Maxime Dénès | 2017-05-11 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | | Remove an unused open introduced by the previous commit. | Maxime Dénès | 2017-05-11 | |
* | | | | | | | | | | | | Merge PR#201: Transparent abstract | Maxime Dénès | 2017-05-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | Switch bedrock to mit-plv base | Jason Gross | 2017-05-10 | |
| | | | | | |/ / / / / / | ||||
| | | | | | * | | | | | | Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print... | Maxime Dénès | 2017-05-10 | |
| | | | | | |\ \ \ \ \ \ | ||||
| | | | | * | | | | | | | | Moving code for miscellaneous tests to specific files. | Hugo Herbelin | 2017-05-10 | |
| | | | | * | | | | | | | | A more regular naming of variables in test-suite Makefile. | Hugo Herbelin | 2017-05-10 | |
| | | | | * | | | | | | | | Adding tests for testing exit status and #use"include". | Hugo Herbelin | 2017-05-10 | |
| | | | | * | | | | | | | | Cleaning old untested not any more interesting testing files. | Hugo Herbelin | 2017-05-10 | |
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | ||||
| | | | | * | | | | | | | Merge PR#591: Add bmsherman/topology to the ci | Maxime Dénès | 2017-05-09 | |
| | | | | |\ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | | Put .travis.yml in alphabetical order | Jason Gross | 2017-05-09 | |
* | | | | | | | | | | | | | Merge PR#619: Fix warnings in top_printers | Maxime Dénès | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#612: Set Ltac Batch Debug | Maxime Dénès | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#606: Added an option Set Debug Cbv | Maxime Dénès | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated. | Maxime Dénès | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#615: coqtop -help: don't die if coqlib can't be found | Maxime Dénès | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * \ \ \ \ \ \ \ | Merge PR#609: Fix bug #3659: -time should understand multibyte encodings. | Maxime Dénès | 2017-05-09 | |
| | | | | | | | | | |\ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | \ \ \ \ \ \ \ \ | Merge PR#617: [toplevel] Fix a couple of logical errors in error printing. | Maxime Dénès | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | | | | | | | | | Prevent user-defined ring morphisms from ever being evaluated. | Guillaume Melquiond | 2017-05-09 | |
| |_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | Fix warnings in top_printers | Gaetan Gilbert | 2017-05-08 | |
| |_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | [toplevel] Fix a couple of logical errors in error printing. | Emilio Jesus Gallego Arias | 2017-05-05 | |
|/ / / / / / / / / / / / / / / / / | ||||
* | | | | | | | | | | | | | | | | | Remove dead code and unused open. | Maxime Dénès | 2017-05-05 | |
* | | | | | | | | | | | | | | | | | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | Maxime Dénès | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | | | | | | | | Remove two unused opens. | Maxime Dénès | 2017-05-05 | |
* | | | | | | | | | | | | | | | | | | Merge PR#598: Removing dead code in Autorewrite. | Maxime Dénès | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | * | | | | | | | | Fix bug #3659: -time should understand multibyte encodings. | Pierre-Marie Pédrot | 2017-05-05 | |
| | | | | | | | | | |/ / / / / / / / | ||||
| | | | | | | | | * | | | | | | | | | Documenting Option.List.find. | Hugo Herbelin | 2017-05-05 |