index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
vernacextend.ml
Age
Commit message (
Expand
)
Author
2020-04-15
[declare] Rename `Declare.t` to `Declare.Proof.t`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-03-25
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Emilio Jesus Gallego Arias
2020-03-25
[parsing] Remove redundant interfaces from Pcoq
Emilio Jesus Gallego Arias
2020-03-25
[parsing] Remove extend AST in favor of gramlib constructors
Emilio Jesus Gallego Arias
2020-03-25
[parsing] Make grammar extension type private.
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-08
[exn] [nit] Remove not very useful re-raises.
Emilio Jesus Gallego Arias
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
2020-02-21
[parsing] Track need to reinit by typing
Emilio Jesus Gallego Arias
2019-10-07
[vernac] Split vernacular translation and interpretation.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-11
STM: encode in static types that vernac_when is only used when VtSideff
Gaëtan Gilbert
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-04
[vernac] Interpret regular vernacs symbolically
Emilio Jesus Gallego Arias
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
Rename Proof_global.{t -> stack}
Gaëtan Gilbert
2019-06-04
Vernacextend only returns a proof_global.t option, not a vernacstate
Gaëtan Gilbert
2019-05-20
Remove VtUnknown classification
Maxime Dénès
2019-03-31
Multiple payload types in tokens
Pierre Roux
2019-03-20
Stop accessing proof env via Pfedit in printers
Maxime Dénès
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-27
Merge PR #8850: Private universes for opaque polymorphic constants.
Matthieu Sozeau
2018-11-23
Remove the unsafe camlp5 API from the Coq codebase.
Pierre-Marie Pédrot
2018-11-23
change vernac_qed_type to have [VtKeep of vernac_keep_as]
Gaëtan Gilbert
2018-11-23
Local universes for opaque polymorphic constants.
Gaëtan Gilbert
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
