index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-10-24
Fix #5763: Strictly positive example is out of order.
jkloos
2017-10-20
Merge PR #5989: Handle ∞ in coq-makefile timing test-suite
Maxime Dénès
2017-10-20
Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just...
Maxime Dénès
2017-10-20
Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974).
Maxime Dénès
2017-10-20
Merge PR #5972: Fixing link to GitHub issue search, and wording.
Maxime Dénès
2017-10-20
Merge PR #1155: Use type nonrec in some functor arguments.
Maxime Dénès
2017-10-20
Merge PR #1147: Remove GeoProof support.
Maxime Dénès
2017-10-20
Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...
Maxime Dénès
2017-10-20
Merge PR #1095: [stm] Remove state handling from Futures
Maxime Dénès
2017-10-20
Merge PR #960: Uniformize references to Bugzilla
Maxime Dénès
2017-10-19
rename ci-iris-coq -> ci-iris-lambda-rust
Ralf Jung
2017-10-19
Handle ∞ in coq-makefile timing test-suite
Jason Gross
2017-10-19
Moving bug numbers to BZ# format in the CHANGES file.
Théo Zimmermann
2017-10-19
Moving bug numbers to BZ# format in the source code.
Théo Zimmermann
2017-10-19
Moving bug numbers to BZ# format in the test-suite.
Théo Zimmermann
2017-10-19
CI: build lambdaRust (which depends on Iris) rather than just Iris
Ralf Jung
2017-10-18
Bugzilla autolink: avoid linking inside links (fix #5974).
Gaëtan Gilbert
2017-10-18
Merge PR #984: Handling primitive projections in canonical structures.
Maxime Dénès
2017-10-18
Fixing link to GitHub issue search, and wording.
Théo Zimmermann
2017-10-18
Merge PR #1149: Moving to GitHub issues.
Maxime Dénès
2017-10-18
Moving to GitHub issues.
Théo Zimmermann
2017-10-17
Adding a test for bug BZ#5692.
Pierre-Marie Pédrot
2017-10-17
unification: fix BZ#5692, recognize prim projs as CS projections
Matthieu Sozeau
2017-10-17
Properly handling projection parameters in canonical structures.
Pierre-Marie Pédrot
2017-10-17
Handling primitive projections in canonical structures.
Pierre-Marie Pédrot
2017-10-17
[vernac] [state] Cache freeze/unfreeze
Emilio Jesus Gallego Arias
2017-10-17
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-10-17
[stm] Move interpretation state to Vernacentries
Emilio Jesus Gallego Arias
2017-10-17
[stm] Remove VtBack from public classification.
Emilio Jesus Gallego Arias
2017-10-17
[stm] First step to move interpretation of Undo commands out of the classifier.
Emilio Jesus Gallego Arias
2017-10-16
Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid`
Maxime Dénès
2017-10-16
Use type nonrec in some functor arguments.
Gaëtan Gilbert
2017-10-16
Merge PR #1152: Fix BZ#5785 (make install -j broken)
Maxime Dénès
2017-10-15
[stdlib] Fix warnings on deprecated `Add Setoid`
Emilio Jesus Gallego Arias
2017-10-13
Fix some more missing mkdir lines to Makefile.ide
Jason Gross
2017-10-13
Fix BZ#5785 (make install -j broken)
Jason Gross
2017-10-13
Merge PR #1103: Take Suggest Proof Using outside the kernel.
Maxime Dénès
2017-10-12
Merge PR #1089: [stm] [toplevel] Move delicate state initialization to the ST...
Maxime Dénès
2017-10-12
Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or directory...
Maxime Dénès
2017-10-11
Remove GeoProof support.
Maxime Dénès
2017-10-11
Merge PR #1054: Restoring test on ident validity while browsing directory str...
Maxime Dénès
2017-10-11
Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every execu...
Maxime Dénès
2017-10-11
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
Emilio Jesus Gallego Arias
2017-10-11
Merge PR #1143: fix coq_makefile on cygwin
Maxime Dénès
2017-10-10
Stm.get_hint_ctx: remove unused Str.split
Gaëtan Gilbert
2017-10-10
Parse [Proof using Type] without translating Type to an id.
Gaëtan Gilbert
2017-10-10
Use a nice printer for constant names in Suggest Proof Using.
Gaëtan Gilbert
2017-10-10
Code factorization Vernacentries.interp on VernacProof.
Gaëtan Gilbert
2017-10-10
[vernac] Remove "Proof using" hacks from parser.
Emilio Jesus Gallego Arias
2017-10-10
Take Suggest Proof Using outside the kernel.
Gaëtan Gilbert
[next]