index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
stm
/
proofBlockDelimiter.ml
Age
Commit message (
Expand
)
Author
2020-09-01
Unify the shelves
Maxime Dénès
2020-08-26
Move given_up goals to evar_map
Maxime Dénès
2020-06-26
[declare] Move proof information to declare.
Emilio Jesus Gallego Arias
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-18
Update headers in the whole code base.
Théo Zimmermann
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-08-14
[vernac] Refactor Vernacular Control Attributes into a list
Emilio Jesus Gallego Arias
2019-06-25
[lemmas] Move `Stack` out of Lemmas.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-05-13
Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.
Hugo Herbelin
2019-05-13
Moving Evd.evars_of_term from constr to econstr + consequences.
Hugo Herbelin
2019-04-25
[vernac] [ast] Make location info an attribute of vernaculars.
Emilio Jesus Gallego Arias
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2018-12-14
[proof] Rework proof interface.
Emilio Jesus Gallego Arias
2018-05-01
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-04-13
Evar maps contain econstrs.
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-01-08
[vernac] vernac_expr no longer recursive
Vincent Laporte
2017-12-20
Separate vernac controls and regular commands.
Maxime Dénès
2017-11-19
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
2017-10-17
[stm] Move interpretation state to Vernacentries
Emilio Jesus Gallego Arias
2017-10-06
[stm] Switch to a functional API
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-10-18
[stm] Fix record field name clash.
Emilio Jesus Gallego Arias
2016-06-07
Documentation
Enrico Tassi
2016-06-06
Error box detection run only on error
Enrico Tassi
2016-06-06
STM: proof block detection for indentation
Enrico Tassi
2016-06-06
STM: proof block detection for par:
Enrico Tassi
2016-06-06
STM: proof block detection for bullets and { block }
Enrico Tassi
