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-14
Merge PR #11978: Close #11935: section variables do not have universe instances.
Pierre-Marie Pédrot
2020-04-14
Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of expli...
Pierre-Marie Pédrot
2020-04-14
Merge PR #12084: [warnings] Be silent about the `set_tag` warning.
Pierre-Marie Pédrot
2020-04-14
Merge PR #12054: [ocamlformat] Update to 0.14.0
Théo Zimmermann
2020-04-13
Merge PR #12089: dune states target: respect user's global verbosity setting
Emilio Jesus Gallego Arias
2020-04-13
[ocamlformat] Update to 0.14.0
Emilio Jesus Gallego Arias
2020-04-13
Close #11935: section variables do not have universe instances.
Gaëtan Gilbert
2020-04-13
Merge PR #11916: [proof] Introduce `prepare_proof` to improve normalization w...
Gaëtan Gilbert
2020-04-13
Merge PR #12081: [test-suite] Remove deprecated -I option of coqchk in Makefile
Gaëtan Gilbert
2020-04-13
Fix #11854 error message on unsolved evars in Instance.
Gaëtan Gilbert
2020-04-13
Remove documentation for Hide menu in CoqIDE (was removed in 8.5).
Théo Zimmermann
2020-04-13
Fix #11783 Require in Section
Gaëtan Gilbert
2020-04-13
Overlay for partial imports
Gaëtan Gilbert
2020-04-13
Update syntax of Import / Export in documentation.
Théo Zimmermann
2020-04-13
doc for partial imports
Gaëtan Gilbert
2020-04-13
Partial import inductive(..)
Gaëtan Gilbert
2020-04-13
always debug validate failures
Gaëtan Gilbert
2020-04-13
test partial import
Gaëtan Gilbert
2020-04-13
syntax for import filters
Gaëtan Gilbert
2020-04-13
correctly open objects for Names filters
Gaëtan Gilbert
2020-04-13
pass filters around
Gaëtan Gilbert
2020-04-13
Add ExtRefMap/Set to globnames
Gaëtan Gilbert
2020-04-13
Add specific test for "useless" syndef
Gaëtan Gilbert
2020-04-13
dune states target: respect user's global verbosity setting
Gaëtan Gilbert
2020-04-13
Merge PR #12087: Temporarily disable Windows job on Azure.
Gaëtan Gilbert
2020-04-13
Temporarily disable Windows job on Azure.
Théo Zimmermann
2020-04-13
Merge PR #11539: [dune] [stdlib] Build the standard library natively with Dune.
Théo Zimmermann
2020-04-13
Simplifying the declaration of constants bound to primitive projections.
Hugo Herbelin
2020-04-12
[warnings] Be silent about the `set_tag` warning.
Emilio Jesus Gallego Arias
2020-04-12
Tweak grammar to make doc_grammar happy
Jim Fehrle
2020-04-12
CoqIDE completion: Relying on INSERT mark of the buffer.
Hugo Herbelin
2020-04-12
Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.
Hugo Herbelin
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
[prev]
[next]