aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-12Fix issue #9175 Windows: VST addon does not work if CompCert is also installedMichael Soegtrop
2018-12-11Merge PR #9197: Fixing imports in debug printers: gramlib depends on Loc ↵Emilio Jesus Gallego Arias
which is in lib.cma
2018-12-11Merge PR #8655: Test suite: use coqc and then coqchkEnrico Tassi
2018-12-11Merge PR #9155: Fix race condition triggered by fresh universe generationEnrico Tassi
2018-12-11Fixing imports in debug printers: gramlib depends on Loc which is in lib.cma.Hugo Herbelin
2018-12-11Merge PR #9151: [dune] Teach coq_dune about `.glob` and `.aux` files.Théo Zimmermann
2018-12-10[test-suite] Fail when the checker failsVincent Laporte
2018-12-10[test-suite] Run `coqchk` on most test casesVincent Laporte
2018-12-10[dune] Teach coq_dune about `.glob` and `.aux` files.Emilio Jesus Gallego Arias
This is a required step in order to be able to call `coqdoc` an generate the documentation of the stdlib, and also useful for other uses such as the asynchronous engine.
2018-12-10Merge PR #9145: Do so that an error message follows the "Error:" header on ↵Emilio Jesus Gallego Arias
the same line
2018-12-10Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.packEmilio Jesus Gallego Arias
2018-12-10Merge PR #9177: add relation-algebra to CI test suiteGaëtan Gilbert
2018-12-10Merge PR #9106: [dune] Install coq libraries in `%{lib_root}/coq` instead of ↵Vincent Laporte
in `lib
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-12-09fix copy-paste error in CI_ARCHIVEURLChristian Doczkal
2018-12-09add relation-algebra to CI test suiteChristian Doczkal
2018-12-08[dune] Install coq libraries in `%{lib_root}/coq` instead of `lib`Emilio Jesus Gallego Arias
This is what the native Dune Coq version already does, but it is a problem for Coq Dune too as noted by @vgbl.
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
2018-12-07Merge PR #8811: EConstr-aware functions to produce kernel entriesPierre-Marie Pédrot
2018-12-06Merge PR #9140: [ci] Add four color theorem proof to CIGaëtan Gilbert
2018-12-06Revise API for global universes.Gaëtan Gilbert
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id. Remove the ability to split the argument of `Univ.Level.Level` into a dirpath*int pair (except by going through string hacks like detyping/pretyping(/funind) does). Id.of_string_soft to turn unnamed universes into qualid is pushed up to detyping. (TODO some followup PR clean up more) This makes it pointless to have an opaque type for ints in Univ.Level: it would only be used as argument to Univ.Level.UGlobal.make, ie ~~~ open Univ.Level let x = UGlobal.make dp (Id.make n) (* vs *) let x = UGlobal.make dp n ~~~ Remaining places which create levels from ints are various hacks (eg the dummy in inductive.ml, the Type.n universes in ugraph sort_universes) and univgen. UnivGen does have an opaque type for ints used as univ ids since they get manipulated by the stm. NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
2018-12-06High level functions to produce kernel entries from econstr.Gaëtan Gilbert
2018-12-06Evarutil.finalize: combine minimize, to_constr and restrict.Gaëtan Gilbert
2018-12-06Rename generated directory gramlib__pack -> gramlib/.packGaëtan Gilbert
It's a bit cleaner this way, especially wrt the number of toplevel directories. Also fix warning about undefined GRAMMARCMA while we're at it.
2018-12-06unignore Makefile.installGaëtan Gilbert
Relevant for gitignore aware tools like ag (silversearcher)
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
Remote counters were trying to build universe levels (as opposed to simple integers), but did not have access to the right dirpath at construction time. We fix it by constructing the level only at use time, and we introduce some abstractions for qualified and unqualified level names.
2018-12-06Merge PR #8917: Small cleanup wrt attributes_of_flags and template attributeVincent Laporte
2018-12-06Merge PR #9069: [gramlib] Remove dead codeHugo Herbelin
2018-12-05[ci] Add four color theorem proof to CIEmilio Jesus Gallego Arias
2018-12-05Remove the Like level modifier from gramlib.Pierre-Marie Pédrot
Apart from the fact we did not use it, its semantics was somewhat flaky as it was looking for any rule containing some token.
2018-12-05Remove the grammar-entry correspondence dynamic check in camlp5.Pierre-Marie Pédrot
Due to the fact we only export the functorial API, this property is ensured statically. There is thus no point in checking it.
2018-12-05Removing dead fields from Plexing.lexer.Pierre-Marie Pédrot
2018-12-05Remove dead code in camlp5.Pierre-Marie Pédrot
The references error_verbose and strict_parsing were not accessible from the API, so their value was statically known.
2018-12-05Remove the lexer field from Gramlib.Pierre-Marie Pédrot
This is useless in the functorial API.
2018-12-05Make some camlp5 fields immutable.Pierre-Marie Pédrot
2018-12-05Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`Pierre-Marie Pédrot
2018-12-05Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.Pierre-Marie Pédrot
2018-12-05Move template out of Defattributes recordGaëtan Gilbert
2018-12-05attributes_of_flags and its output type now internal in vernacentriesGaëtan Gilbert
2018-12-05Merge PR #8911: Document undocumented flags and optionsThéo Zimmermann
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
Also remove a few undocumented settings
2018-12-04Remove undocumented "Proof using Clear Unused" flagJim Fehrle
2018-12-04Merge PR #9134: CI: track dev branch of coq-simple-ioEmilio Jesus Gallego Arias
2018-12-04CI: track dev branch of coq-simple-ioYishuai Li
2018-12-04Merge PR #9127: Remove leftover code that used to handle ml4 files.Emilio Jesus Gallego Arias
2018-12-04Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes)Emilio Jesus Gallego Arias
2018-12-04Remove leftover code that used to handle ml4 files.Pierre-Marie Pédrot
2018-12-04Merge PR #9053: Document code owner team creation.Maxime Dénès
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
Namely, it does not explicitly open a scope, but we remember that we don't need the %type delimiter when in type position.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:40:40 +0000