index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
coqpp
Age
Commit message (
Expand
)
Author
2019-07-19
Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files
Jim Fehrle
2019-06-17
Update headers of files that were stuck on older headers.
Théo Zimmermann
2019-06-05
Merge PR #10215: Refine typing of vernacular commands
Maxime Dénès
2019-06-05
allow empty tactic_rules in ARGUMENT EXTEND
Dabrowski
2019-06-04
[vernac] remove VtMaybeOpenProof
Enrico Tassi
2019-06-04
VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)
Gaëtan Gilbert
2019-06-04
Replace ModifyProofStack by CloseProof
Gaëtan Gilbert
2019-06-04
Vernacextend only returns a proof_global.t option, not a vernacstate
Gaëtan Gilbert
2019-06-04
Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof
Gaëtan Gilbert
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-05-21
Fixing typos - Part 1
JPR
2019-04-02
Add parsing of decimal constants (e.g., 1.02e+01)
Pierre Roux
2019-04-02
Rename the INT token to NUMERAL
Pierre Roux
2019-03-31
Improve coqpp error message for SELF in anonymous entry
Pierre Roux
2019-03-31
Multiple payload types in tokens
Pierre Roux
2019-03-31
[parsing] add keyword-protected generic quotation
Enrico Tassi
2019-03-31
[parsing] Split Tok.t into Tok.t and Tok.pattern
Enrico Tassi
2019-03-27
[coqpp] [ltac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-03-20
Stop accessing proof env via Pfedit in printers
Maxime 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-23
Only use Coq API in coqpp.
Pierre-Marie Pédrot
2018-11-17
[vernacextend] Consolidate extension points API
Emilio Jesus Gallego Arias
2018-11-13
[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.
Emilio Jesus Gallego Arias
2018-11-02
coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax
Gaëtan Gilbert
2018-10-15
Implement ARGUMENT EXTEND in coqpp.
Pierre-Marie Pédrot
2018-10-11
Merge PR #8161: Implement VERNAC EXTEND in coqpp
Maxime Dénès
2018-10-03
[dune] Add `(package coq)` scope to artifacts.
Emilio Jesus Gallego Arias
2018-10-02
Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.
Pierre-Marie Pédrot
2018-10-02
Handling VERNAC EXTEND in coqpp.
Pierre-Marie Pédrot
2018-10-02
Pass unnamed arguments to ML macros.
Pierre-Marie Pédrot
2018-10-01
Print location in OCaml code output by coqpp.
Pierre-Marie Pédrot
2018-10-01
Store locations of OCaml quotations in coqpp.
Pierre-Marie Pédrot
2018-09-06
deprecation is CODE instead of IDENT
Vincent Laporte
2018-09-06
coqpp: allow DEPRECATED when declaring tactics
Vincent Laporte
2018-09-05
[build] Preliminary support for building Coq with `dune`.
Emilio Jesus Gallego Arias
2018-07-25
Fix static declaration of plugins in coqpp.
Pierre-Marie Pédrot
2018-07-11
[coqpp] Move to its own directory.
Emilio Jesus Gallego Arias
