index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
declare.mli
Age
Commit message (
Expand
)
Author
2020-06-03
[declare] Hide internals of variable declaration entries.
Emilio Jesus Gallego Arias
2020-05-26
[declare] Turn restrict_ucontext hack into an internal parameter
Emilio Jesus Gallego Arias
2020-05-26
[declare] Don't expose internal parameter obls
Emilio Jesus Gallego Arias
2020-05-26
[declare] Simplify exported type of definition_entry
Emilio Jesus Gallego Arias
2020-05-20
[obligations] `declare_obligation` now takes an `UState.t`
Emilio Jesus Gallego Arias
2020-05-20
[declare] [nit] Use proper type alias for in ProgramDecl interface
Emilio Jesus Gallego Arias
2020-05-20
[nit] Remove `Declare.Obls.err_not_transp`
Emilio Jesus Gallego Arias
2020-05-19
[declare] Remove unused parameters in prepare_obligation
Emilio Jesus Gallego Arias
2020-05-18
[declare] Grand unification of the proof save path.
Emilio Jesus Gallego Arias
2020-05-18
[declare] Merge `DeclareObl` into `Declare`
Emilio Jesus Gallego Arias
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-05-07
[declare] Remove fix_exn internal access.
Emilio Jesus Gallego Arias
2020-05-03
[funind] Remove use of low-level entries in scheme generation.
Emilio Jesus Gallego Arias
2020-04-21
[declare] [compat] Add alias for deprecated function
Emilio Jesus Gallego Arias
2020-04-21
[declare] Remove `declare_private_constant` from the public API.
Emilio Jesus Gallego Arias
2020-04-21
[declare] [tactics] Move declare to `vernac`
Emilio Jesus Gallego Arias
