aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-01Teach coq_dune about the empty .vos produced by coqcGaëtan Gilbert
Without this the next dune command after build a vo will wipe out the vos, breaking interactive users. Also this means dune installs the .vos files.
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01[make] install .vos along with .voEnrico Tassi
2019-11-01fix installation of vos files in coq Makefilecharguer
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall ↵charguer
that the generation of a .vo files induces the creation of an empty .vos file.)
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01Changelog entryMaxime Dénès
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file.
2019-11-01Merge PR #11015: [Nix] Update reference to nixpkgsThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-31Merge PR #11021: Fix build in masterPierre-Marie Pédrot
2019-10-31lra: use “lia” rather than “omega”Vincent Laporte
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
Ack-by: fajb Reviewed-by: ppedrot
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
`Prettyp` is now late enough in linking to refer to them.
2019-10-31Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”Pierre-Marie Pédrot
2019-10-31Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-31Merge PR #11000: make: guard cp calls with rm -f on executablesPierre-Marie Pédrot
Reviewed-by: gares
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
Ack-by: SkySkimmer Ack-by: proux01 Reviewed-by: vbgl
2019-10-31Merge PR #10997: Implement the unsupported attribute error using the warning ↵Emilio Jesus Gallego Arias
system Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-31QArith: only depend on ZArith_baseVincent Laporte
2019-10-31Zdigits: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zquot: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zpow_facts: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zwf: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zgcd_alt: use “lia” rather than “omega”Vincent Laporte
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31ppvernac: bidi hints use & not |Gaëtan Gilbert
2019-10-31Print argument info as an Arguments command in AboutGaëtan Gilbert
Close #10961
2019-10-31Move prettyp (Print implementation) to vernac/Gaëtan Gilbert
2019-10-31Doc: index command Arguments with assertGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: jfehrle
2019-10-31Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them ↵Pierre-Marie Pédrot
unique names Reviewed-by: ppedrot
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-31Merge PR #10933: Add clarification in make-changelog.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-10-31[Nix] Update reference to nixpkgsVincent Laporte
This version of nixpkgs includes: - Dune 1.11.4 - GTK3 3.24.12 - menhir 20190626
2019-10-30Merge PR #10953: [declare] Remove declare_scheme hook in DeclarePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-30Merge PR #10999: [refman] Give an example of contradiction when positivity ↵Clément Pit-Claudel
checking is disabled. Reviewed-by: cpitclaudel
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
Noticed by coverage, test code by Gäetan Gilbert. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-10-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
This means we can disable it to ignore unsupported attributes. For instance this would be useful if we change some behaviour of `Cmd` and add an attribute `att` to restore the old behaviour, then `#[att] Cmd` is backwards compatible if the warning is disabled.
2019-10-30Use bullets and indentation (but the result rendering is weird).Théo Zimmermann
2019-10-30Use explicit match as suggested by Clément.Théo Zimmermann
2019-10-30[refman] Add a second example of contradiction when positivity checking is ↵Théo Zimmermann
disabled.
2019-10-30Make changelog script aware of trailing slashes.Arthur Azevedo de Amorim
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:23:52 +0000