aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-25Merge PR #6642: fix space in coqchk errorMaxime Dénès
2018-01-25Merge PR #6650: Remove dead code from funind.Maxime Dénès
2018-01-25Merge PR #6626: [readme] Add DOI badge.Maxime Dénès
2018-01-25Merge PR #6620: Fix #6591: anomaly when using selectors outside of a proof.Maxime Dénès
2018-01-24fix space in coqchk errorRalf Jung
2018-01-24Remove dead code from funind.Maxime Dénès
2018-01-24Fix #6621: Anomaly on fixpoint with primitive projectionsMaxime Dénès
The implementation of the subterm relation for primitive projections was a bit wrong. I found the problem independently of this bug, and tried to see if a proof of False could be derived, but I don't think so, due to another check (check_is_subterm) that saves the kernel at the last minute.
2018-01-23Delay installing packagesJason Gross
sudo apt-get install will fail on gcc-multilib if apt-get update cannot fetch launchpad, so instead we delay installing these packages.
2018-01-23Use travis_retry on apt-get updateJason Gross
Script modified from https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status I stuck the code in "install" rather than "before_install" so that the lint target didn't need to be changed. I also haven't touched the targets that add more packages; I'll leave that to someone who knows more about the "&" and "*" syntax being used in the configuration.
2018-01-23Stop running duplicate Travis jobs on pull requests.Théo Zimmermann
These tests are already done by CircleCI.
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Maxime Dénès
for primitive projections
2018-01-23Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and ↵Maxime Dénès
pr_lname
2018-01-23Merge PR #6629: Archive COMPATIBILITYMaxime Dénès
2018-01-23Merge PR #6568: Cleanup scriptsMaxime Dénès
2018-01-22Fix #6591: anomaly when using selectors outside of a proof.Cyprien Mangin
When asking for a hint about bullets, we check that there is an ongoing proof.
2018-01-22[readme] Add DOI badge.Emilio Jesus Gallego Arias
2018-01-22Archive COMPATIBILITY.Théo Zimmermann
2018-01-22Move the mention of the removal of Qed exporting at the right place.Théo Zimmermann
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6625: Update location on tab switch, issue 6624Maxime Dénès
2018-01-22Merge PR #6576: generate both binary and text annotationsMaxime Dénès
2018-01-22Merge PR #6550: Remove outdated note about rlwrap in setup.txtMaxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-22Merge PR #6575: Add flash infos for find and replaceMaxime Dénès
2018-01-22Merge PR #6506: Fast rel lookupMaxime Dénès
2018-01-22[printing] Remove duplicate definitions of pr_lident and pr_lnameVincent Laporte
2018-01-20Adding a test for coqchk bug #6619.Pierre-Marie Pédrot
2018-01-20Fix #6618: coqchk fails with "ill-typed term".Pierre-Marie Pédrot
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.
2018-01-20Remove dead code in Environ.Pierre-Marie Pédrot
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.
2018-01-19-annotate deprecated. New options: -annot, -bin-annotVadim Zaliva
2018-01-19update location on tab switch, issue 6624Paul Steckler
2018-01-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-19Fix context handling of fix and cofix in Ltac subterm matching.Cyprien Mangin
2018-01-19Define EConstr version of [push_rec_types].Cyprien Mangin
2018-01-18add flash infos about wrap, not found, no. of replacements, no. of finds, ↵Paul Steckler
issue #6452
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-18Merge PR #6448: Cleanup and add debug printers a bitMaxime Dénès
2018-01-17Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < ↵Maxime Dénès
2.18.3
2018-01-17Merge PR #6593: Add plugins to META.coqMaxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Merge PR #6584: Implement the strategy mechanism in the checkerMaxime Dénès
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
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).
2018-01-16Update lablgtk check to be more generalJason Gross
2018-01-16Rename coq.ltac to coq.plugins.ltac in META.coqCyprien Mangin
2018-01-16Update configure.ml to only warn on lablgtk 2.16.0Jason Gross
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
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-08 16:09:23 +0000