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-26
[declare] Return list of declared global in Proof.save
Emilio Jesus Gallego Arias
2020-06-26
[declare] Some more cleanup on unused functions after the last commits.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Remove Proof_ending from the public API
Emilio Jesus Gallego Arias
2020-06-26
[declare] Merge remaining obligations bits into Declare
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] Use Recthm.t in mutual analysis functions
Emilio Jesus Gallego Arias
2020-06-26
[declare] Refactor analysis and construction of mutual lemmas
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on interface
Emilio Jesus Gallego Arias
2020-06-26
[declare] Documentation on obligations
Emilio Jesus Gallego Arias
2020-06-26
[declare] [compat] Remove exception alias.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Modify logical presentation of declare interfaces
Emilio Jesus Gallego Arias
2020-06-26
[declare] Reify Proof.t API into the Proof module.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Move udecl to Info structure.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Removal of duplicated type aliases.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Removal of deprecated functions
Emilio Jesus Gallego Arias
2020-06-26
[declare] Make ProgramDecl.t abstract
Emilio Jesus Gallego Arias
2020-06-26
[declare] Refactor constant information into a record.
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-06-26
[declare] Stronger typing for start_proof
Emilio Jesus Gallego Arias
2020-06-11
[declare] Remove some unused `fix_exn`
Emilio Jesus Gallego Arias
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
