aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
Improve debug output
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-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-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.
2018-12-04Notation.ml: Moving code about binding scopes to coercion classes earlier.Hugo Herbelin
We shall need it for changing the semantics of type_scope.
2018-12-04Fixing missing newline in display of Locate for notations.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
This modifies the strategy in previous commits so that priorities are as before in case of non-open scopes with delimiters. Additionally, we document the rare situation of overlapping applicative notations (maybe this is too rare and ad hoc to be worth being documented though).
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
Mostly courtesy of Jason Gross.
2018-12-04Using scope for printing: more tests.Hugo Herbelin
2018-12-04Fixing #8551 (missing delimiters when notation exists both lonely and in scope).Hugo Herbelin
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
We do a couple of changes: - Splitting notation keys into more categories to make table smaller. This should (a priori) make printing faster (see #6416). - Abbreviations are treated for printing like single notations: they are pushed to the scope stack, so that in a situation such as Open Scope foo_scope. Notation foo := term. Open Scope bar_scope. one looks for notations first in scope bar_scope, then try to use foo, they try for notations in scope foo_scope. - We seize the opportunity of this commit to simplify availability_of_notation which is now integrated to uninterp_notation and which does not have to be called explicitly anymore.
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
See discussion on coq-club starting on 23 August 2016.
2018-12-04Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2018-12-03Merge PR #9121: Closes #9118: single backticks are made equivalent to double ↵Clément Pit-Claudel
backticks; try to fix all misuses.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:12:59 +0000