Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop) | 2018-01-17 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6584: Implement the strategy mechanism in the checker | 2018-01-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | Add CHANGES entry | 2018-01-17 | ||
| | | | | | | | | | * | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction | 2018-01-17 | ||
| | | | | | * | | | | | | Add CHANGES entry | 2018-01-17 | ||
| | | | | | * | | | | | | Add a test that `prod_applist_assum` reduces the right number of let-ins | 2018-01-17 | ||
| | | | | | * | | | | | | Use let-in aware prod_applist_assum in dtauto and firstorder. | 2018-01-17 | ||
| | | | | | | |_|_|/ / | | | | | | |/| | | | | ||||
| | | | * | | | | | | | Update lablgtk check to be more general | 2018-01-16 | ||
| | | * | | | | | | | | Rename coq.ltac to coq.plugins.ltac in META.coq | 2018-01-16 | ||
| | | | * | | | | | | | Update configure.ml to only warn on lablgtk 2.16.0 | 2018-01-16 | ||
| | | | | |/ / / / / | | | | |/| | | | | | ||||
| | | | | | | | | * | merge-pr.sh: use git diff --quiet | 2018-01-16 | ||
| | | | | | | | | * | Source basic overlay before user overlays. | 2018-01-16 | ||
| | | | | | | | | * | Cleanup shell expansions and quoting. | 2018-01-16 | ||
| | | | | | | | | * | Simplify logic and streamline lint-repository.sh | 2018-01-16 | ||
* | | | | | | | | | | Merge PR #6590: Fix the wrapper around ocamldebug. | 2018-01-16 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr | 2018-01-16 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6466: Replace md5sum/md5 calls by an OCaml program | 2018-01-16 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6551: Bracket with goal selector | 2018-01-16 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | Add plugins to META.coq | 2018-01-16 | ||
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | ||||
| | | | * | | | | | | | | Fix the wrapper around ocamldebug. | 2018-01-15 | ||
| |_|_|/ / / / / / / / |/| | | | | | | | | | | ||||
| | * | | | | | | | | | Avoid shell backticks and improve md5sum.ml error messages | 2018-01-15 | ||
| * | | | | | | | | | | More tests on brackets with goal selectors (including failures). | 2018-01-15 | ||
| * | | | | | | | | | | Add test-suite file for bracket with goal selector. | 2018-01-15 | ||
| | | | * | | | | | | | Actually use the strategy information in the checker. | 2018-01-14 | ||
| | | | * | | | | | | | Store the conversion oracle in constant and inductive definitions. | 2018-01-14 | ||
| |_|_|/ / / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #6578: Remove references to deleted Unicode.Unsupported exception | 2018-01-13 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6581: Added newline at the end of usage of coqdep. | 2018-01-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | 2018-01-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6483: Strong invariants in polymorphic definitions | 2018-01-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6288: Interfaces for checker and IDE. | 2018-01-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | Adding a custom Travis overlay for HoTT. | 2018-01-11 | ||
| | * | | | | | | | | | | | | | Enforce that polymorphic definitions do not generate internal constraints. | 2018-01-11 | ||
| | | * | | | | | | | | | | | | Document test-suite PRINT_LOGS. | 2018-01-11 | ||
| | | * | | | | | | | | | | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | 2018-01-11 | ||
| |_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | Merge PR #6557: First stab at documenting the test suite. | 2018-01-11 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6552: [PR template] Remove the relative link to CHANGES. | 2018-01-11 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | Added newline at the end of usage of coqdep. | 2018-01-11 | ||
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | Force polymorphic definitions to have no internal constraints. | 2018-01-11 | ||
| | | | | * | | | | | | | | | Remove references to removed Unicode.Unsupported | 2018-01-11 | ||
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | Lint and remove redundant line | 2018-01-11 | ||
| | | * | | | | | | | | | | Add interfaces for IDE and remove dead code. | 2018-01-10 | ||
| | | * | | | | | | | | | | Add interfaces for checker and remove dead code. | 2018-01-10 | ||
| |_|/ / / / / / / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label | 2018-01-10 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6570: [meta] Fix typo on Coq's META file following #6444. | 2018-01-10 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | Add comments by @psteckler to test-suite/README.md | 2018-01-10 | ||
| * | | | | | | | | | | | | [meta] Fix typo on Coq's META file following #6444. | 2018-01-09 | ||
|/ / / / / / / / / / / / | ||||
| | | | | | | | | | | * | Cleanup conditional in lint-repository.sh | 2018-01-08 | ||
| | | | | | | | | | * | | Stop talking about debian in "A note about rlwrap" | 2018-01-08 | ||
| | | | | | | | | | |/ | ||||
| | | | | | * | | | | | [vernac] vernac_expr no longer recursive | 2018-01-08 | ||
* | | | | | | | | | | | Merge PR #6532: Fix mli-doc issue #6531 | 2018-01-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ |