index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-11-01
Merge PR #8642: Compiled interfaces with -vos and -vok options
Pierre-Marie Pédrot
2019-11-01
Merge PR #11019: enforcing Ltac2 constructor name are uppercased
Pierre-Marie Pédrot
2019-11-01
adding test file for Uppercase Ltac2 constructors
Kenji Maillard
2019-11-01
enforcing Ltac2 cosntructors name are uppercase in open types
Kenji Maillard
2019-11-01
Add warnings regarding the experimental nature of the vos feature in the doc.
Pierre-Marie Pédrot
2019-11-01
Teach coq_dune about the empty .vos produced by coqc
Gaëtan Gilbert
2019-11-01
[test-suite] acknowledge coq_mafile installs .vos
Enrico Tassi
2019-11-01
[make] install .vos along with .vo
Enrico Tassi
2019-11-01
fix installation of vos files in coq Makefile
charguer
2019-11-01
a tentative patch to allow interactive session to load .vos files; (recall th...
charguer
2019-11-01
fix coq_makefile and doc for vos support.
charguer
2019-11-01
Changelog entry
Maxime Dénès
2019-11-01
additional details in the doc for -vos
charguer
2019-11-01
Implementing support for vos/vok files.
charguer
2019-11-01
Merge PR #11015: [Nix] Update reference to nixpkgs
Théo Zimmermann
2019-10-31
Merge PR #11021: Fix build in master
Pierre-Marie Pédrot
2019-10-31
lra: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArith
Pierre-Marie Pédrot
2019-10-31
Merge PR #10985: Print argument info as an Arguments command in About
Emilio Jesus Gallego Arias
2019-10-31
[prettyp] remove `mod_ops` and `indirect_accessor` parameters
Gaëtan Gilbert
2019-10-31
enforcing Ltac2 constructor name are uppercased
Kenji Maillard
2019-10-31
Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”
Pierre-Marie Pédrot
2019-10-31
Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”
Pierre-Marie Pédrot
2019-10-31
Merge PR #11000: make: guard cp calls with rm -f on executables
Pierre-Marie Pédrot
2019-10-31
Merge PR #9883: Add support for Sorts in numeral notations
Vincent Laporte
2019-10-31
Merge PR #10997: Implement the unsupported attribute error using the warning ...
Emilio Jesus Gallego Arias
2019-10-31
lia: depend only on ZArith_base
Vincent Laporte
2019-10-31
QArith: only depend on ZArith_base
Vincent Laporte
2019-10-31
Zdigits: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zquot: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zpow_facts: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zwf: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
Zgcd_alt: use “lia” rather than “omega”
Vincent Laporte
2019-10-31
restore red behaviour printing
Gaëtan Gilbert
2019-10-31
changelog for #10985
Gaëtan Gilbert
2019-10-31
Fix output tests
Gaëtan Gilbert
2019-10-31
ppvernac: bidi hints use & not |
Gaëtan Gilbert
2019-10-31
Print argument info as an Arguments command in About
Gaëtan Gilbert
2019-10-31
Move prettyp (Print implementation) to vernac/
Gaëtan Gilbert
2019-10-31
Doc: index command Arguments with assert
Gaëtan Gilbert
2019-10-31
Move Arguments implementation to its own file (from vernacentries)
Gaëtan Gilbert
2019-10-31
Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.
Gaëtan Gilbert
2019-10-31
Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them uniqu...
Pierre-Marie Pédrot
2019-10-31
Merge PR #10995: add test for #4502 (fixed by unknown commit)
Pierre-Marie Pédrot
2019-10-31
Merge PR #10933: Add clarification in make-changelog.
Gaëtan Gilbert
2019-10-31
[Nix] Update reference to nixpkgs
Vincent Laporte
2019-10-30
Merge PR #10953: [declare] Remove declare_scheme hook in Declare
Pierre-Marie Pédrot
2019-10-30
Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.
Pierre-Marie Pédrot
2019-10-30
Rename the 2 local type_cstr nonterminals to give them unique names
Jim Fehrle
2019-10-30
Merge PR #10999: [refman] Give an example of contradiction when positivity ch...
Clément Pit-Claudel
[next]