index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
pfedit.ml
Age
Commit message (
Expand
)
Author
2020-04-15
[proofs] Move pfedit to `proofs`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Move proof_global functionality to Proof_global from Pfedit
Emilio Jesus Gallego Arias
2020-04-06
Clean and fix definitions of options.
Théo Zimmermann
2020-03-31
[proof] Split delayed and regular proof closing functions, part II
Emilio Jesus Gallego Arias
2020-03-19
[pfedit] Labelize sign parameter
Emilio Jesus Gallego Arias
2020-03-19
[declare] Remaining bits on the consistency of UState.t naming
Emilio Jesus Gallego Arias
2020-03-19
[declare] Remove one use of inline_private_constants
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-02-12
Remove Goptions.opt_name field
Gaëtan Gilbert
2020-01-30
[exn] Don't reraise in exception printers
Emilio Jesus Gallego Arias
2019-10-30
Merge PR #10949: [declare] Provide helper for private constant inlining.
Pierre-Marie Pédrot
2019-10-30
Merge PR #10681: [declare] Make `proof_entry` a private type.
Pierre-Marie Pédrot
2019-10-29
Show diffs in "Show Proof."
Jim Fehrle
2019-10-29
[declare] Make `proof_entry` a private type.
Emilio Jesus Gallego Arias
2019-10-28
[declare] Provide helper for private constant inlining.
Emilio Jesus Gallego Arias
2019-10-09
Specialize UState.merge for extend:false
Gaëtan Gilbert
2019-10-09
Simplify universe handling wrt side effects: rm demote_seff_univs
Gaëtan Gilbert
2019-08-27
[declare] Move proof_entry type to declare, put interactive proof data on top...
Emilio Jesus Gallego Arias
