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
2021-01-14
Merge PR #13378: Add support for high resolution timeout functions
Pierre-Marie Pédrot
2021-01-12
Add an indirection to the UGraph internal representation.
Pierre-Marie Pédrot
2021-01-06
Further pushing up the printing and sorting of universes.
Pierre-Marie Pédrot
2021-01-05
Move universe printing out of AcyclicGraph.
Pierre-Marie Pédrot
2020-12-06
Add support for high resolution timeout functions.
Lasse Blaauwbroek
2020-12-04
[win] [envars] honor file "coq_environment.txt"
Enrico Tassi
2020-12-04
[coq_makefile] honor environment for OCAMLFIND
Enrico Tassi
2020-11-25
Separate interning and pretyping of universes
Gaëtan Gilbert
2020-11-23
Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...
Pierre-Marie Pédrot
2020-11-22
Fix timeout by ensuring signal exceptions are not erroneously caught
Lasse Blaauwbroek
2020-11-20
Add default value of -native-compiler to `coqc -config`
Pierre Roux
2020-11-02
Merge PR #13250: Micro-optimization in Control.check_for_interrupt.
coqbot-app[bot]
2020-10-27
Rename misc nonterminals
Jim Fehrle
2020-10-27
Rename tactic_expr -> ltac_expr
Jim Fehrle
2020-10-22
Micro-optimization in Control.check_for_interrupt.
Pierre-Marie Pédrot
2020-10-12
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol
coqbot-app[bot]
2020-10-09
Add an XML message for "Show Proof Diffs"
Jim Fehrle
2020-10-08
Dropping the misleading int argument of Pp.h.
Hugo Herbelin
2020-09-17
Be more efficient when generating the merge of ltle maps in AcyclicGraph.
Pierre-Marie Pédrot
2020-09-17
Do not allocate intermediate sets in universe refreshing.
Pierre-Marie Pédrot
2020-07-10
Fix #12513: coq no longer reports mismatched version numbers.
Pierre-Marie Pédrot
2020-06-11
[declare] Remove some unused `fix_exn`
Emilio Jesus Gallego Arias
2020-05-15
[misc] Better preserve backtraces in several modules
Emilio Jesus Gallego Arias
2020-05-13
Centralize the OCaml version-checking function.
Pierre-Marie Pédrot
2020-04-26
Open object files in binary mode.
Pierre-Marie Pédrot
2020-04-26
Tweak a comment on the low-level objfile API.
Pierre-Marie Pédrot
2020-04-26
Move the ObjFile module to its own file.
Pierre-Marie Pédrot
2020-04-26
Implement a name-based representation for vo files.
Pierre-Marie Pédrot
2020-04-08
[errors] Print backtrace of internal errors in printers
Emilio Jesus Gallego Arias
2020-04-01
Merge PR #11306: Centralize the flag handling native compilation.
Maxime Dénès
2020-03-30
Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creation
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-13
[cleanup] Remove unnecessary Map/Set module creation
Emilio Jesus Gallego Arias
2020-03-11
Merge PR #11790: [lib] [ccalgo] Remove unused code / cleanup
Pierre-Marie Pédrot
2020-03-10
[clib] Remove module CStack
Emilio Jesus Gallego Arias
2020-03-08
[exn] [nit] Remove not very useful re-raises.
Emilio Jesus Gallego Arias
2020-03-08
Merge PR #11578: [exn] Keep information from multiple extra exn handlers
Pierre-Marie Pédrot
2020-03-03
[exn] Keep information from multiple extra exn handlers
Emilio Jesus Gallego Arias
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
2020-02-24
[exn] Generate an anomaly if the exn printer raises.
Emilio Jesus Gallego Arias
2020-02-24
[exn] Forbid raising in exn printers, make them return Pp.t option
Emilio Jesus Gallego Arias
2020-01-15
[ocaml] Remove Custom Backtrace module in favor of OCaml's
Emilio Jesus Gallego Arias
2019-12-22
Centralize the flag handling native compilation.
Pierre-Marie Pédrot
2019-12-12
Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...
charguer
2019-12-02
Remove deprecated compat modifier of Notation / Infix commands.
Théo Zimmermann
2019-11-27
[release] Update files for 8.12 release per release process.
Emilio Jesus Gallego Arias
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-11-11
Run update-compat script with --release option.
Théo Zimmermann
2019-11-01
Implementing support for vos/vok files.
charguer
2019-10-07
Call to update-compat.py.
Pierre-Marie Pédrot
[next]