index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
vernacstate.ml
Age
Commit message (
Expand
)
Author
2020-11-20
[stm] [declare] Remove pinfo internals hack.
Emilio Jesus Gallego Arias
2020-08-31
Update update_global_env usage
Gaëtan Gilbert
2020-08-27
[state] A few nits after consolidation of state.
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Functionalize Program state
Emilio Jesus Gallego Arias
2020-07-01
[state] Consolidate state handling in Vernacstate
Emilio Jesus Gallego Arias
2020-06-26
[declare] Improve logical code order
Emilio Jesus Gallego Arias
2020-06-26
[declare] Improve organization of proof/constant information.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Reify Proof.t API into the Proof module.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Remove mutual internals from Info.t structure.
Emilio Jesus Gallego Arias
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-04-15
[proof] Move proof_global functionality to Proof_global from Pfedit
Emilio Jesus Gallego Arias
2020-03-31
[proof] [stm] Force `opaque` in `close_future_proof`
Emilio Jesus Gallego Arias
2020-03-31
[proof] Split return_proof in partial and regular versions.
Emilio Jesus Gallego Arias
2020-03-31
[proof] Split delayed and regular proof closing functions, part II
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-24
[exn] Forbid raising in exn printers, make them return Pp.t option
Emilio Jesus Gallego Arias
2020-01-30
[exn] Don't reraise in exception printers
Emilio Jesus Gallego Arias
2019-06-25
[lemmas] Move `Stack` out of Lemmas.
Emilio Jesus Gallego Arias
2019-06-24
[lemmas] Turn Lemmas.info into a proper type with constructor.
Emilio Jesus Gallego Arias
2019-06-24
[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.
Emilio Jesus Gallego Arias
2019-06-20
Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...
Pierre-Marie Pédrot
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-17
[proof] drop parameter from terminator type
Emilio Jesus Gallego Arias
2019-06-17
[proofs] Store hooks in the proof object.
Emilio Jesus Gallego Arias
2019-06-09
[proof] Uniformize Proof_global API
Emilio Jesus Gallego Arias
2019-06-09
[save_proof] Make terminator API internal.
Emilio Jesus Gallego Arias
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-04
Rename Proof_global.{t -> stack}
Gaëtan Gilbert
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-03-27
[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.
Emilio Jesus Gallego Arias
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-12-21
Fix shallow flag in vernac state
Maxime Dénès
2018-12-13
Move shallow state logic to the function preparing state for workers
Maxime Dénès
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-04
[vernac] Couple of tweaks missing from previous PRs.
Emilio Jesus Gallego Arias
2017-11-29
[proof] [api] Rename proof types in preparation for functionalization.
Emilio Jesus Gallego Arias
2017-11-22
[plugin] Encapsulate modifiers to vernac commands.
Emilio Jesus Gallego Arias
2017-11-19
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
