index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
proof_global.mli
Age
Commit message (
Expand
)
Author
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] Fixme on unused return type.
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-30
[proof] Miscellaneous cleanup on proof info handling
Emilio Jesus Gallego Arias
2020-03-25
[proof] Start of mutual definition save refactoring.
Emilio Jesus Gallego Arias
2020-03-19
[proof] Remove duplicated poly field in Proof_global.t
Emilio Jesus Gallego Arias
2020-03-19
[declare] Remaining bits on the consistency of UState.t naming
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-11-08
Make [Proof_global.closed_proof_output] opaque
Gaëtan Gilbert
2019-10-04
Remove redundancy in section hypotheses of kernel entries.
Pierre-Marie Pédrot
2019-08-27
[declare] Move proof_entry type to declare, put interactive proof data on top...
Emilio Jesus Gallego Arias
