index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
declare.ml
Age
Commit message (
Expand
)
Author
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-08
Don't suggest Proof using when no section variables
Gaëtan Gilbert
2020-06-03
[declare] Hide internals of variable declaration entries.
Emilio Jesus Gallego Arias
2020-05-26
[declare] Split univs_poly_private in close_proof
Emilio Jesus Gallego Arias
2020-05-26
[declare] Factor common universe computation in close proof.
Emilio Jesus Gallego Arias
2020-05-26
[declare] Split univs_deferred in close_proof
Emilio Jesus Gallego Arias
2020-05-26
[declare] Factor out universe computation in close_proof
Emilio Jesus Gallego Arias
2020-05-26
[declare] Nit on errors.
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
Merge PR #12356: [declare] Remove unused parameters in prepare_obligation
Gaëtan Gilbert
2020-05-19
[declare] Remove unused parameters in prepare_obligation
Emilio Jesus Gallego Arias
2020-05-19
[declare] Minor tweaks in prepare_obligation
Emilio Jesus Gallego Arias
2020-05-19
[declare] Remove dead code in prepare_obligation
Emilio Jesus Gallego Arias
2020-05-19
[universes] [api] Provide UState.from_env
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-09
Merge PR #12241: [declare] Merge DeclareDef into Declare
Gaëtan Gilbert
2020-05-08
Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpoints
Pierre-Marie Pédrot
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-05-01
Changing fixpoint message "decreasing" -> "guarded".
Hugo Herbelin
2020-04-30
Remove outdated code and comments in Declare.
Pierre-Marie Pédrot
2020-04-21
[declare] [compat] Add alias for deprecated function
Emilio Jesus Gallego Arias
2020-04-21
[declare] [tactics] Move declare to `vernac`
Emilio Jesus Gallego Arias
[prev]
