aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-10For diffs, return exactly the characters that make up STRING and FIELD tokensJim Fehrle
2018-12-10Fix #9091: don't show deleted compacted hypotheses twice in diffJim Fehrle
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
Improve debug output
2018-12-10[coq] Adapt to coq/coq#9172Emilio Jesus Gallego Arias
Note that this highlights some issues with the current Coq interface, not clear what should we do.
2018-12-10List members of the code of conduct enforcement team.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-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
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 pull request coq/ltac2#90 from ejgallego/testsPierre-Marie Pédrot
[build] Test tests in Travis, use coqc for tests.
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 pull request #20 from ejgallego/vernac+remove_empty_hooksEmilio Jesús Gallego Arias
[coq overlay] Adapt to coq/coq#8705
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-05Add test for #8951.Gaëtan Gilbert
Close #8951.
2018-12-05Fix mod_subst wrt universe polymorphismGaë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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 18:22:44 +0000