aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-31Merge PR #6601: Circle CI: fix cache selection.Maxime Dénès
2018-01-31Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m...Maxime Dénès
2018-01-31Merge PR #6663: [toplevel] Refactor load path handling.Maxime Dénès
2018-01-31Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Maxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-30Put default value for NJOBS in ci-common.Gaëtan Gilbert
2018-01-30Adding an overlay for Equations.Pierre-Marie Pédrot
2018-01-30Merge PR #6666: Fix reduction of primitive projections on coinductive records...Maxime Dénès
2018-01-30Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsMaxime Dénès
2018-01-30Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Maxime Dénès
2018-01-30Merge PR #6605: Safer VM interfacesMaxime Dénès
2018-01-30Merge PR #6644: Use travis_retry on apt-get updateMaxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-29[cbv] Fix evaluation of cofixpoints under primitive projections.Maxime Dénès
2018-01-29[native_compute] Fix evaluation of cofixpoints under primitive projections.Maxime Dénès
2018-01-29[toplevel] Refactor load path handling.Emilio Jesus Gallego Arias
2018-01-26Safer VM interfacesMaxime Dénès
2018-01-25Add test case for #5747Maxime Dénès
2018-01-25[checker] Avoid relying on canonical names.Maxime Dénès
2018-01-25[checker] Remove duplicated functionMaxime Dénès
2018-01-25[checker] Better error message for bad recursive treesMaxime Dénès
2018-01-25Add a comment referencing travis issue numbersJason Gross
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
2018-01-23Delay installing packagesJason Gross
2018-01-23Use travis_retry on apt-get updateJason Gross
2018-01-23Stop running duplicate Travis jobs on pull requests.Théo Zimmermann
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Maxime Dénès
2018-01-23Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and pr_l...Maxime Dénès
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
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