aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-08pre-commit: add files after fixing ending newlines.Gaëtan Gilbert
2018-02-08Document configure setting up pre-commit hook in CONTRIBUTING.mdGaëtan Gilbert
2018-02-08Have the pre-commit hook also fix end-of-file nlJason Gross
2018-02-08Auto-create .git/hooks/pre-commit on ./configureJason Gross
2018-02-08pre-commit hook: fix whitespace error detectionGaëtan Gilbert
2018-02-08Mention linter and pre-commit hook in CONTRIBUTING.md.Gaëtan Gilbert
2018-02-08A pre-commit hook to magically fix whitespace issues.Gaëtan Gilbert
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-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
2018-01-20Remove dead code in Environ.Pierre-Marie Pédrot
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, iss...Paul Steckler
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 < 2...Maxime Dénès
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
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
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
2018-01-16Source basic overlay before user overlays.Gaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
2018-01-16Merge PR #6590: Fix the wrapper around ocamldebug.Maxime Dénès
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès