aboutsummaryrefslogtreecommitdiff
path: root/coqpp
AgeCommit message (Expand)Author
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-07-08[obligations] Allow to simultaneously open a proof and add obligationsEmilio Jesus Gallego Arias
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-05-09NumTok.int doesn't exist anymorePierre Roux
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-05Merge PR #10215: Refine typing of vernacular commandsMaxime Dénès
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04[vernac] remove VtMaybeOpenProofEnrico Tassi
2019-06-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)Gaëtan Gilbert
2019-06-04Replace ModifyProofStack by CloseProofGaëtan Gilbert
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-05-21Fixing typos - Part 1JPR
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-04-02Rename the INT token to NUMERALPierre Roux
2019-03-31Improve coqpp error message for SELF in anonymous entryPierre Roux
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-31[parsing] add keyword-protected generic quotationEnrico Tassi
2019-03-31[parsing] Split Tok.t into Tok.t and Tok.patternEnrico Tassi
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
2018-11-23Only use Coq API in coqpp.Pierre-Marie Pédrot
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
2018-10-15Implement ARGUMENT EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-03[dune] Add `(package coq)` scope to artifacts.Emilio Jesus Gallego Arias
2018-10-02Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.Pierre-Marie Pédrot
2018-10-02Handling VERNAC EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
2018-10-01Print location in OCaml code output by coqpp.Pierre-Marie Pédrot
2018-10-01Store locations of OCaml quotations in coqpp.Pierre-Marie Pédrot
2018-09-06deprecation is CODE instead of IDENTVincent Laporte
2018-09-06coqpp: allow DEPRECATED when declaring tacticsVincent Laporte
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-07-25Fix static declaration of plugins in coqpp.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:37:38 +0000