aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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
2018-12-06unignore Makefile.installGaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
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
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
2018-12-05Remove the grammar-entry correspondence dynamic check in camlp5.Pierre-Marie Pédrot
2018-12-05Removing dead fields from Plexing.lexer.Pierre-Marie Pédrot
2018-12-05Remove dead code in camlp5.Pierre-Marie Pédrot
2018-12-05Remove the lexer field from Gramlib.Pierre-Marie Pédrot
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
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
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
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
2018-12-04Notation.ml: Moving code about binding scopes to coercion classes earlier.Hugo Herbelin
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
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
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
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
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
2018-12-03[sphinx] Same rendering for :n:`@token` and :token:`token`.Théo Zimmermann
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 01:44:50 +0000