Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Aligning on standard layout of CHANGES. | 2017-05-13 | |
* | Merge PR#594: An example showing the benefit of Econstr | 2017-05-11 | |
|\ | |||
* \ | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a... | 2017-05-11 | |
|\ \ | |||
* \ \ | Merge PR#572: Replacing costly merges in UGraph. | 2017-05-11 | |
|\ \ \ | |||
* | | | | Remove an unused open introduced by the previous commit. | 2017-05-11 | |
* | | | | Merge PR#201: Transparent abstract | 2017-05-11 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#619: Fix warnings in top_printers | 2017-05-09 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#612: Set Ltac Batch Debug | 2017-05-09 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#606: Added an option Set Debug Cbv | 2017-05-09 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated. | 2017-05-09 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR#615: coqtop -help: don't die if coqlib can't be found | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR#617: [toplevel] Fix a couple of logical errors in error printing. | 2017-05-09 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | Prevent user-defined ring morphisms from ever being evaluated. | 2017-05-09 | |
| |_|/ / / / / / / / |/| | | | | | | | | | |||
| | | | | * | | | | | Fix warnings in top_printers | 2017-05-08 | |
| |_|_|_|/ / / / / |/| | | | | | | | | |||
| * | | | | | | | | [toplevel] Fix a couple of logical errors in error printing. | 2017-05-05 | |
|/ / / / / / / / | |||
* | | | | | | | | Remove dead code and unused open. | 2017-05-05 | |
* | | | | | | | | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | 2017-05-05 | |
|\ \ \ \ \ \ \ \ | |||
* | | | | | | | | | Remove two unused opens. | 2017-05-05 | |
* | | | | | | | | | Merge PR#598: Removing dead code in Autorewrite. | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | Documenting Option.List.find. | 2017-05-05 | |
| | | | | | | | | * | Cosmetic: unifying style within option.ml. | 2017-05-05 | |
| | | | | | | | | * | Upgrading some local function as a general-purpose combinator Option.List.map. | 2017-05-05 | |
| | | | | | | | | * | Adding a test-suite pattern-unification example that Econstr fixed. | 2017-05-05 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
* | | | | | | | | | Merge PR#610: Improve documentation of assert / pose proof / specialize. | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR#605: Report a useful error for dependent induction | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | coqtop -help: don't die if coqlib can't be found | 2017-05-05 | |
| |_|_|_|/ / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR#454: Printing unfocussed goals and toward a pg plugin. | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#593: Functional choice <-> [inhabited] and [forall] commute | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | | Remove unused open. | 2017-05-05 | |
* | | | | | | | | | | | | Merge PR#544: Anonymous universes | 2017-05-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | | | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat... | 2017-05-04 | |
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | |||
| | | | | * | | | | | | | Improve documentation of assert / pose proof / specialize. | 2017-05-04 | |
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | |||
| | | * | | | | | | | | Warning removed. | 2017-05-04 | |
| | | * | | | | | | | | labelizing arguments | 2017-05-04 | |
| | | * | | | | | | | | Adding an option "Printing Unfocused". | 2017-05-04 | |
| |_|/ / / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR#541: Fixing "decide equality" bug #5449 | 2017-05-03 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#588: Allow interactive editing of {C,}Morphisms in PG | 2017-05-03 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#386: Better editing of the standard library in coqtop/PG | 2017-05-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#602: Fix more warnings | 2017-05-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#404: patch for printing types of let bindings | 2017-05-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | * | | | | Added an option Set Debug Cbv. | 2017-05-03 | |
| |_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | |||
| | | | | | | | * | | | | | | Report a useful error for dependent induction | 2017-05-03 | |
| |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | |||
| | | | | | | * | | | | | | Reorganize comment documentation of ChoiceFacts.v | 2017-05-03 | |
| | | | | | * | | | | | | | Type@{_} should not produce a flexible algebraic universe. | 2017-05-03 | |
| | | | | | * | | | | | | | Allow flexible anonymous universes in instances and sorts. | 2017-05-03 | |
* | | | | | | | | | | | | | Merge PR#411: Mention template polymorphism in the documentation. | 2017-05-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | |||
| | * | | | | | | | | | | | applied the patch for printing types of let bindings by @herbelin | 2017-05-02 | |
| |/ / / / / / / / / / / |/| | | | | | | | | | | | |||
| | * | | | | | | | | | | Remove dead code in native compiler. | 2017-05-02 | |
| | * | | | | | | | | | | Fix two new unused opens. | 2017-05-02 | |
| | * | | | | | | | | | | Remove unused module definition after merging PR#592. | 2017-05-02 | |
| |/ / / / / / / / / / |/| | | | | | | | | | |