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-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
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-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
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-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-04
typo
Enrico Tassi
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
Switching to an untyped toplevel representation for Ltac values.
Pierre-Marie Pédrot
2016-05-02
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-25
Print magic numbers in bad magic error message
Tej Chajed
2016-04-20
Adding an OCaml printer for pre-initialization anomalies.
Pierre-Marie Pédrot
2016-04-15
Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.
Hugo Herbelin
2016-04-09
In pr_clauses, do not print a leading space by default so that it can
Hugo Herbelin
2016-04-08
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-03-30
Ensuring that the type of base generic arguments contain triples.
Pierre-Marie Pédrot
2016-03-30
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-30
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-22
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-19
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-19
Removing the untyped representation of genargs.
Pierre-Marie Pédrot
2016-03-18
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-17
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
Reducing the number of modules linked in grammar.cma.
Pierre-Marie Pédrot
2016-03-15
Fix #4591: Uncaught exception in directory browsing.
Pierre-Marie Pédrot
2016-03-13
Adding a few functions on type union.
Hugo Herbelin
[next]