Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for... | 2018-01-23 | |
|\ | |||
* \ | Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and pr_l... | 2018-01-23 | |
|\ \ | |||
* \ \ | Merge PR #6629: Archive COMPATIBILITY | 2018-01-23 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6568: Cleanup scripts | 2018-01-23 | |
|\ \ \ \ | |||
| | * | | | Archive COMPATIBILITY. | 2018-01-22 | |
| | * | | | Move the mention of the removal of Qed exporting at the right place. | 2018-01-22 | |
* | | | | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | 2018-01-22 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6625: Update location on tab switch, issue 6624 | 2018-01-22 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6576: generate both binary and text annotations | 2018-01-22 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6550: Remove outdated note about rlwrap in setup.txt | 2018-01-22 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6575: Add flash infos for find and replace | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6506: Fast rel lookup | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |||
| | | | | | | | | * | | [printing] Remove duplicate definitions of pr_lident and pr_lname | 2018-01-22 | |
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | |||
| | | | | | | | | * | Adding a test for coqchk bug #6619. | 2018-01-20 | |
| | | | | | | | | * | Fix #6618: coqchk fails with "ill-typed term". | 2018-01-20 | |
| | | | | | | | | * | Remove dead code in Environ. | 2018-01-20 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| | | | | * | | | | -annotate deprecated. New options: -annot, -bin-annot | 2018-01-19 | |
| | | | | | * | | | update location on tab switch, issue 6624 | 2018-01-19 | |
| |_|_|_|_|/ / / |/| | | | | | | | |||
| | | * | | | | | Add test-suite file for issue #6617. | 2018-01-19 | |
| | | * | | | | | Fix context handling of fix and cofix in Ltac subterm matching. | 2018-01-19 | |
| | | * | | | | | Define EConstr version of [push_rec_types]. | 2018-01-19 | |
| | * | | | | | | add flash infos about wrap, not found, no. of replacements, no. of finds, iss... | 2018-01-18 | |
| |/ / / / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | 2018-01-18 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6448: Cleanup and add debug printers a bit | 2018-01-18 | |
|\ \ \ \ \ \ \ \ | |_|_|/ / / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2... | 2018-01-17 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6593: Add plugins to META.coq | 2018-01-17 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | 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 |