index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
proof_global.ml
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-04-10
[sideeff] Don't use polymorphic equality to check for empty side-effects
Emilio Jesus Gallego Arias
2020-04-10
[proof] Introduce `prepare_proof` to improve normalization workflow.
Emilio Jesus Gallego Arias
2020-04-06
Clean and fix definitions of options.
Théo Zimmermann
2020-03-31
[proof] Improve comment and argument name.
Emilio Jesus Gallego Arias
2020-03-31
[proof] [stm] Force `opaque` in `close_future_proof`
Emilio Jesus Gallego Arias
2020-03-31
[proof] Remove unused parameter in the delayed save path.
Emilio Jesus Gallego Arias
2020-03-31
[proof] Fixme on unused return type.
Emilio Jesus Gallego Arias
2020-03-31
[proof] Remove internal wrapper in Proof_global
Emilio Jesus Gallego Arias
2020-03-31
[proof] Minor refactorings in Proof_global
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-31
[proof] Split delayed and regular proof closing functions, part I
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
2020-02-12
Remove Goptions.opt_name field
Gaëtan Gilbert
2019-10-29
[declare] Make `proof_entry` a private type.
Emilio Jesus Gallego Arias
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
