index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-04-12
Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common.
Hugo Herbelin
2020-04-12
[test-suite] Remove deprecated -I option of coqchk in Makefile
Pierre Roux
2020-04-11
[dune] [doc] Remove the quick targets in favor of the shims.
Emilio Jesus Gallego Arias
2020-04-11
[dune] [stdlib] Build the standard library natively with Dune.
Emilio Jesus Gallego Arias
2020-04-11
[ci] [build] Bump Dune to 2.5.0
Emilio Jesus Gallego Arias
2020-04-11
[gitlab-ci] Only run Windows jobs when ONLY_WINDOWS variable is true.
Théo Zimmermann
2020-04-11
Merge PR #11961: Convert vernac commands chapter to prodn, update syntax
Théo Zimmermann
2020-04-11
add properties of operations on vectors
Olivier Laurent
2020-04-11
Fix #7812
Attila Gáspár
2020-04-11
If a custom entry has global, a bound variable is valid in this entry.
Hugo Herbelin
2020-04-11
If a custom entry has global, an argument-free abbreviation is valid in this ...
Hugo Herbelin
2020-04-11
Renaming confusingly-named insert_coercion into insert_entry_coercion.
Hugo Herbelin
2020-04-10
Convert vernac commands chapter to prodn, update syntax
Jim Fehrle
2020-04-10
coqdoc: Report location of mismatched '[['
Lysxia
2020-04-10
[sideeff] Don't use polymorphic equality to check for empty side-effects
Emilio Jesus Gallego Arias
2020-04-10
[proof] Introduce `prepare_proof` to improve normalization workflow.
Emilio Jesus Gallego Arias
2020-04-10
Suppress the space after "#" when printing productions
Jim Fehrle
2020-04-10
Ignore subscripts in notation for matching cmds and tacs
Jim Fehrle
2020-04-10
Fix prefix matching
Jim Fehrle
2020-04-10
Merge PR #12039: Do not erase native files in debug mode
Pierre-Marie Pédrot
2020-04-10
Merge PR #11882: Adding a short form of Ltac2 Fresh.fresh
Pierre-Marie Pédrot
2020-04-10
Merge PR #11756: [lib] Remove custom backtrace-destroying finalizers
Pierre-Marie Pédrot
2020-04-10
Change log for #12068 (Coqide segfault tentative fix).
Hugo Herbelin
2020-04-10
Coqide completion: Avoiding using an iterator in an apparently sensitive code.
Hugo Herbelin
2020-04-10
Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-crypto
Gaëtan Gilbert
2020-04-10
[obligations] Deprecated flag cleanup
Emilio Jesus Gallego Arias
2020-04-10
[ocamlformat] Enable for funind.
Emilio Jesus Gallego Arias
2020-04-09
Merge PR #12010: Remove dead code in Evarsolve alias algorithm
Hugo Herbelin
2020-04-09
Code simplification in find_projectable_vars.
Pierre-Marie Pédrot
2020-04-09
Remove a unused computation in alias code.
Pierre-Marie Pédrot
2020-04-09
Inline an alias-computing function only used once.
Pierre-Marie Pédrot
2020-04-09
Remove dead code in Evarsolve alias resolution.
Pierre-Marie Pédrot
2020-04-09
Merge PR #12046: [errors] Print backtrace of internal errors in printers
Pierre-Marie Pédrot
2020-04-09
Merge PR #11534: Support universe bindings and universe constraints in Let de...
Gaëtan Gilbert
2020-04-09
Merge PR #12056: [pre-commit] Check ocamlformat version and silence ocamlformat.
Gaëtan Gilbert
2020-04-09
Merge PR #12050: Fix a typo in CoqMakefile.in
Pierre-Marie Pédrot
2020-04-09
[pre-commit] Check ocamlformat version and silence ocamlformat.
Théo Zimmermann
2020-04-08
Merge PR #12044: proposed fix for the issue #12015 (String_as_OT)
Jason Gross
2020-04-08
[ci] [fiat-crypto] [flambda] Don't use flambda for fiat-crypto
Emilio Jesus Gallego Arias
2020-04-08
Merge PR #11909: Make the level of ≡ in Int63 consistent with =
Hugo Herbelin
2020-04-08
Fix a typo in CoqMakefile.in
Jason Gross
2020-04-08
[errors] Print backtrace of internal errors in printers
Emilio Jesus Gallego Arias
2020-04-08
Merge PR #12005: Remove deprecated coqtop options
Emilio Jesus Gallego Arias
2020-04-07
Merge PR #11997: Clean and fix definitions of options.
Emilio Jesus Gallego Arias
2020-04-07
Integrated changes proposed by @JasonGross
ilya
2020-04-07
proposed fix for the issue #12015 (String_as_OT)
ilya
2020-04-07
Support universe bindings and universe constraints in Let definitions.
Théo Zimmermann
2020-04-07
Merge PR #12042: Fix documentation of Print Libraries following #10476.
Clément Pit-Claudel
2020-04-07
Fix documentation of Print Libraries following #10476.
Théo Zimmermann
2020-04-07
Do not erase native files in debug mode
Maxime Dénès
[prev]
[next]