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-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-15
Fix the wrapper around ocamldebug.
Pierre-Marie Pédrot
2018-01-15
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-14
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-13
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
Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS
Maxime Dénès
2018-01-12
Merge PR #6483: Strong invariants in polymorphic definitions
Maxime Dénès
2018-01-12
Merge PR #6288: Interfaces for checker and IDE.
Maxime Dénès
2018-01-11
Adding a custom Travis overlay for HoTT.
Pierre-Marie Pédrot
2018-01-11
Enforce that polymorphic definitions do not generate internal constraints.
Pierre-Marie Pédrot
2018-01-11
Document test-suite PRINT_LOGS.
Gaëtan Gilbert
2018-01-11
Fix undefined variables in test-suite/Makefile + add PRINT_LOGS
Gaëtan Gilbert
2018-01-11
Merge PR #6557: First stab at documenting the test suite.
Maxime Dénès
2018-01-11
Merge PR #6552: [PR template] Remove the relative link to CHANGES.
Maxime Dénès
2018-01-11
Added newline at the end of usage of coqdep.
Bernhard Schommer
2018-01-11
Force polymorphic definitions to have no internal constraints.
Pierre-Marie Pédrot
2018-01-11
Remove references to removed Unicode.Unsupported
Jasper Hugunin
2018-01-11
Lint and remove redundant line
Jasper Hugunin
2018-01-10
Add interfaces for IDE and remove dead code.
Maxime Dénès
2018-01-10
Add interfaces for checker and remove dead code.
Maxime Dénès
2018-01-10
Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label
Maxime Dénès
2018-01-10
Merge PR #6570: [meta] Fix typo on Coq's META file following #6444.
Maxime Dénès
2018-01-10
Add comments by @psteckler to test-suite/README.md
Jasper Hugunin
2018-01-09
[meta] Fix typo on Coq's META file following #6444.
Emilio Jesus Gallego Arias
2018-01-08
Cleanup conditional in lint-repository.sh
Gaëtan Gilbert
2018-01-08
Stop talking about debian in "A note about rlwrap"
Gaëtan Gilbert
2018-01-08
[vernac] vernac_expr no longer recursive
Vincent Laporte
2018-01-08
Merge PR #6532: Fix mli-doc issue #6531
Maxime Dénès
2018-01-08
Merge PR #6489: Update PNGs; mention async error handling; change query windo...
Maxime Dénès
2018-01-08
Merge PR #6497: Add optimize_heap tactic for #6488
Maxime Dénès
2018-01-08
Merge PR #6549: Normalize package names
Maxime Dénès
2018-01-08
Merge PR #6533: Update the lower-bound of the lablgtk dependency.
Maxime Dénès
2018-01-08
Merge PR #6425: Cleanup universes in the kernel
Maxime Dénès
2018-01-08
Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts
Maxime Dénès
2018-01-08
Merge PR #6530: Ignore generated test-suite/output/MExtraction.out
Maxime Dénès
2018-01-08
Merge PR #6517: Trim more trailing whitespace in coq-makefile timing test
Maxime Dénès
2018-01-08
Merge PR #6527: Update backport script for more control.
Maxime Dénès
2018-01-08
Merge PR #6526: Fixing various typos in the Credits chapter.
Maxime Dénès
2018-01-08
github-check-prs.py: print PR URLs when needed.
Gaëtan Gilbert
2018-01-08
github-check-prs.py: Strip spaces from token from command line
Gaëtan Gilbert
2018-01-08
github-check-prs.py: command line option to get token from a file
Gaëtan Gilbert
2018-01-08
Merge PR #6510: Document between and exists_between types.
Maxime Dénès
2018-01-08
Document between and exists_between types.
Ismail
2018-01-08
Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06
Maxime Dénès
[prev]
[next]