Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | | | | | 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 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Primitive projections were not correctly unfolded, leading to failure of conversion checks in some cases. The kernel was strangely not affected by this bug, and it was probably a remnant of some vestigial code. | |||
| | | | | | | | | * | | | Remove dead code in Environ. | Pierre-Marie Pédrot | 2018-01-20 | |
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The constant_value function was actually not behaving the same as constant_value_in w.r.t. projections. The former was not used, and the only place that used the latter was in Tacred and was statically insensitive to the use of projections. | |||
| | | | | * | | | | | | -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, ↵ | Paul Steckler | 2018-01-18 | |
| |/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | issue #6452 | |||
* | | | | | | | | | 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 < ↵ | Maxime Dénès | 2018-01-17 | |
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 2.18.3 | |||
* \ \ \ \ \ \ \ \ \ \ | 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 | |
| | | | | | | |_|_|/ / / / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt). | |||
| | | | * | | | | | | | | | 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 | |
| | | | | |/ / / / / / / | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0 even for much newer versions. This makes building Coq on Ubuntu impossible without modifying configure. This commit fixes that problem. See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for the upstream bug. This closes #6585 | |||
| | | | | | | | | * | | | 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 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation. | |||
* | | | | | | | | | | | | 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 | |
| |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | Fix the wrapper around ocamldebug. | Pierre-Marie Pédrot | 2018-01-15 | |
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug | |||
| | * | | | | | | | | | | | Avoid shell backticks and improve md5sum.ml error messages | Jacques-Pascal Deplaix | 2018-01-15 | |
| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | More tests on brackets with goal selectors (including failures). | Théo Zimmermann | 2018-01-15 | |
| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Add test-suite file for bracket with goal selector. | Théo Zimmermann | 2018-01-15 | |
| | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | Actually use the strategy information in the checker. | Pierre-Marie Pédrot | 2018-01-14 | |
| | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | Store the conversion oracle in constant and inductive definitions. | Pierre-Marie Pédrot | 2018-01-14 | |
| |_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet. | |||
* | | | | | | | | | | | | Merge PR #6578: Remove references to deleted Unicode.Unsupported exception | Maxime Dénès | 2018-01-13 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6581: Added newline at the end of usage of coqdep. | Maxime Dénès | 2018-01-13 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ |