index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-02-08
pre-commit: add files after fixing ending newlines.
Gaëtan Gilbert
2018-02-08
Document configure setting up pre-commit hook in CONTRIBUTING.md
Gaëtan Gilbert
2018-02-08
Have the pre-commit hook also fix end-of-file nl
Jason Gross
2018-02-08
Auto-create .git/hooks/pre-commit on ./configure
Jason Gross
2018-02-08
pre-commit hook: fix whitespace error detection
Gaëtan Gilbert
2018-02-08
Mention linter and pre-commit hook in CONTRIBUTING.md.
Gaëtan Gilbert
2018-02-08
A pre-commit hook to magically fix whitespace issues.
Gaëtan Gilbert
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-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-20
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-19
-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-18
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-17
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-16
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
[next]