Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | | | | | Use travis_retry on apt-get update | Jason Gross | 2018-01-23 | |
| |_|/ / / / / |/| | | | | | | ||||
| | | * | | | | Stop running duplicate Travis jobs on pull requests. | Théo Zimmermann | 2018-01-23 | |
| |_|/ / / / |/| | | | | | ||||
* | | | | | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for... | Maxime Dénès | 2018-01-23 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and pr_l... | Maxime Dénès | 2018-01-23 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #6629: Archive COMPATIBILITY | Maxime Dénès | 2018-01-23 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #6568: Cleanup scripts | Maxime Dénès | 2018-01-23 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | Fix #6591: anomaly when using selectors outside of a proof. | Cyprien Mangin | 2018-01-22 | |
| | | | | | |_|_|/ | | | | | |/| | | | ||||
| | | | | | * | | | [readme] Add DOI badge. | Emilio Jesus Gallego Arias | 2018-01-22 | |
| | | | | |/ / / | ||||
| | * | | | | | | Archive COMPATIBILITY. | Théo Zimmermann | 2018-01-22 | |
| | * | | | | | | Move the mention of the removal of Qed exporting at the right place. | Théo Zimmermann | 2018-01-22 | |
| | | |_|/ / / | | |/| | | | | ||||
* | | | | | | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #6625: Update location on tab switch, issue 6624 | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #6576: generate both binary and text annotations | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #6550: Remove outdated note about rlwrap in setup.txt | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6575: Add flash infos for find and replace | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6506: Fast rel lookup | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | [printing] Remove duplicate definitions of pr_lident and pr_lname | Vincent Laporte | 2018-01-22 | |
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | | | | | | | * | | | Adding a test for coqchk bug #6619. | Pierre-Marie Pédrot | 2018-01-20 | |
| | | | | | | | | * | | | Fix #6618: coqchk fails with "ill-typed term". | Pierre-Marie Pédrot | 2018-01-20 | |
| | | | | | | | | * | | | Remove dead code in Environ. | Pierre-Marie Pédrot | 2018-01-20 | |
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | ||||
| | | | | * | | | | | | -annotate deprecated. New options: -annot, -bin-annot | Vadim Zaliva | 2018-01-19 | |
| | | | | | * | | | | | update location on tab switch, issue 6624 | Paul Steckler | 2018-01-19 | |
| |_|_|_|_|/ / / / / |/| | | | | | | | | | ||||
| | | * | | | | | | | Add test-suite file for issue #6617. | Cyprien Mangin | 2018-01-19 | |
| | | * | | | | | | | Fix context handling of fix and cofix in Ltac subterm matching. | Cyprien Mangin | 2018-01-19 | |
| | | * | | | | | | | Define EConstr version of [push_rec_types]. | Cyprien Mangin | 2018-01-19 | |
| | * | | | | | | | | add flash infos about wrap, not found, no. of replacements, no. of finds, iss... | Paul Steckler | 2018-01-18 | |
| |/ / / / / / / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | Maxime Dénès | 2018-01-18 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #6448: Cleanup and add debug printers a bit | Maxime Dénès | 2018-01-18 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2... | Maxime Dénès | 2018-01-17 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6593: Add plugins to META.coq | Maxime Dénès | 2018-01-17 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop) | Maxime Dénès | 2018-01-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6584: Implement the strategy mechanism in the checker | Maxime Dénès | 2018-01-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | Add CHANGES entry | Jasper Hugunin | 2018-01-17 | |
| | | | | | | | | | * | | | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction | Jasper Hugunin | 2018-01-17 | |
| | | | | | * | | | | | | | | Add CHANGES entry | Jasper Hugunin | 2018-01-17 | |
| | | | | | * | | | | | | | | Add a test that `prod_applist_assum` reduces the right number of let-ins | Jasper Hugunin | 2018-01-17 | |
| | | | | | * | | | | | | | | Use let-in aware prod_applist_assum in dtauto and firstorder. | Jasper Hugunin | 2018-01-17 | |
| | | | | | | |_|_|/ / / / | | | | | | |/| | | | | | | ||||
| | | | * | | | | | | | | | Update lablgtk check to be more general | Jason Gross | 2018-01-16 | |
| | | * | | | | | | | | | | Rename coq.ltac to coq.plugins.ltac in META.coq | Cyprien Mangin | 2018-01-16 | |
| | | | * | | | | | | | | | Update configure.ml to only warn on lablgtk 2.16.0 | Jason Gross | 2018-01-16 | |
| | | | | |/ / / / / / / | | | | |/| | | | | | | | ||||
| | | | | | | | | * | | | merge-pr.sh: use git diff --quiet | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | | * | | | Source basic overlay before user overlays. | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | | * | | | Cleanup shell expansions and quoting. | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | | * | | | Simplify logic and streamline lint-repository.sh | Gaëtan Gilbert | 2018-01-16 | |
* | | | | | | | | | | | | Merge PR #6590: Fix the wrapper around ocamldebug. | Maxime Dénès | 2018-01-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr | Maxime Dénès | 2018-01-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6466: Replace md5sum/md5 calls by an OCaml program | Maxime Dénès | 2018-01-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6551: Bracket with goal selector | Maxime Dénès | 2018-01-16 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | Add plugins to META.coq | Cyprien Mangin | 2018-01-16 | |
| |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |