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
2021-02-25
[proof using] Remove duplicate code, refactor.
Emilio Jesus Gallego Arias
2020-11-26
[declare] Allow custom typing flags when declaring constants.
Emilio Jesus Gallego Arias
2020-11-20
[stm] [declare] Remove pinfo internals hack.
Emilio Jesus Gallego Arias
2020-11-20
[stm] [declare] Try to propagate safe bits of proof information
Emilio Jesus Gallego Arias
2020-11-02
[stm] support #[using] attribute
Enrico Tassi
2020-11-02
document Proof.compact
Enrico Tassi
2020-11-02
attribute #[using] for Definition and Fixpoint
Enrico Tassi
2020-08-31
Update update_global_env usage
Gaëtan Gilbert
2020-08-20
[vernac] refine check for unresolved evars
Enrico Tassi
2020-07-15
[search] Don't use ad-hoc Dumpglob table for Search
Emilio Jesus Gallego Arias
2020-07-08
declare: Add [save_regular] API for obligation-ignoring proofs
Gaëtan Gilbert
2020-07-08
[declare] Allow obligations update on equations closing hook.
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Allow state-modifying hooks
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Functionalize Program state
Emilio Jesus Gallego Arias
2020-07-08
[declare] Generalize type of hooks.
Emilio Jesus Gallego Arias
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
[next]
