index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
Age
Commit message (
Expand
)
Author
2016-08-19
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-09
Make List.map_filter(_i) tail-recursive.
Guillaume Melquiond
2016-07-08
Fixing the printing of unknown locations by adding a newline.
Pierre-Marie Pédrot
2016-07-08
Adding a breaking space in warning names.
Pierre-Marie Pédrot
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-29
A new infrastructure for warnings.
Maxime Dénès
2016-06-27
Merge remote-tracking branch 'github/pr/223' into feedback-locations
Maxime Dénès
2016-06-27
add CList.extract_first
Gabriel Scherer
2016-06-25
[feedback] Remove `ErrorMsg` in favor of `Message Error`.
Emilio Jesus Gallego Arias
2016-06-25
[feedback] Allow messages to carry a location.
Emilio Jesus Gallego Arias
2016-06-25
[feedback] Add optional ?loc parameter to loggers.
Emilio Jesus Gallego Arias
2016-06-25
[feedback] Remove unused tag on `Debug` level.
Emilio Jesus Gallego Arias
2016-06-20
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-06-17
remote counter: avoid thread race on sockets (fix #4823)
Enrico Tassi
2016-06-17
remote counter: avoid thread race on sockets (fix #4823)
Enrico Tassi
2016-06-16
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-14
Preventive compatibility fixes for flushing.
Emilio Jesus Gallego Arias
2016-06-14
Merge remote-tracking branch 'origin/pr/166' into trunk
Enrico Tassi
2016-06-14
-async-proofs-delegation-threshold default value set to 0.03
Enrico Tassi
2016-06-14
Merge remote-tracking branch 'origin/pr/182' into trunk
Enrico Tassi
2016-06-14
Merge remote-tracking branch 'origin/pr/173' into trunk
Enrico Tassi
2016-06-14
Add a [CList.partitioni] function.
Cyprien Mangin
2016-06-14
Merge branch "LtacProf for trunk" (PR #165).
Pierre-Marie Pédrot
2016-06-14
Moving back Ltac profiling to the Ltac folder.
Pierre-Marie Pédrot
2016-06-14
Moving UTF-8 related functions to Unicode module.
Pierre-Marie Pédrot
2016-06-13
Revert "Strip some trailing spaces"
Pierre-Marie Pédrot
2016-06-09
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-07
Documentation
Enrico Tassi
2016-06-06
STM: each proof block can be enabled separately
Enrico Tassi
2016-06-06
STM: proof block detection made optional + simple test
Enrico Tassi
2016-06-06
STM: support for nested boxes of nodes to model error boundaries
Enrico Tassi
2016-06-05
LtacProf for Coq trunk
Jason Gross
2016-06-05
Strip some trailing spaces
Jason Gross
2016-06-04
Merge remote-tracking branch 'github/pr/184' into trunk
Maxime Dénès
2016-06-02
Please never mention .mli-only file in *.mllib (or future *.mlpack)
Pierre Letouzey
2016-06-02
Add documentation to the low-level `Pp` functions.
Emilio Jesus Gallego Arias
2016-06-02
Move ide serialization libraries from lib/ to ide/
Emilio Jesus Gallego Arias
2016-06-02
Encapsulate xml serialization in xmlprotocol.mli
Emilio Jesus Gallego Arias
2016-06-02
Remove tabulation support from pretty-printing.
Guillaume Melquiond
2016-06-01
Merge branch 'yet-another-makefile-bigbang' into trunk
Pierre Letouzey
2016-06-01
Makefile: restore the use of coqdep_boot for creating .v.d files
Pierre Letouzey
2016-05-31
STM delegation policy can be customized
Enrico Tassi
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-19
Unicode.ascii_of_ident is now truly injective
Pierre Letouzey
2016-05-19
Unicode.ascii_of_ident is now truly injective
Pierre Letouzey
2016-05-19
coqc: support -o option to specify output file name
Enrico Tassi
2016-05-13
Dyn: simplify API introducing an Easy submodule
Enrico Tassi
2016-05-12
Fix bug #4722: Coq dies when encountering broken symbolic links.
Pierre-Marie Pédrot
2016-05-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
[prev]
[next]