index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
declare.ml
Age
Commit message (
Expand
)
Author
2019-08-16
Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...
SimonBoulier
2019-08-08
Emit Feedback.AddedAxiom in Declare instead of higher layers
Gaëtan Gilbert
2019-07-31
Specialize the section API.
Pierre-Marie Pédrot
2019-07-31
Remove the universe part from the section variable mechanism.
Pierre-Marie Pédrot
2019-07-08
Similar purity invariants in the kernel.
Pierre-Marie Pédrot
2019-07-08
Further cleanup following the removal of pure opaque definitions.
Pierre-Marie Pédrot
2019-07-08
Do not export side-effects of polymorphic definitions.
Pierre-Marie Pédrot
2019-07-03
declare_variable: path is always Lib.cwd()
Gaëtan Gilbert
2019-07-03
Remove unused Decls.variable_{context,polymorphic}
Gaëtan Gilbert
2019-07-03
Declare section variables in direct style "without" an object
Gaëtan Gilbert
2019-07-03
Move declare_universe_context to top of Declare
Gaëtan Gilbert
2019-07-03
Safe_typing.push_named_assum: don't take universes
Gaëtan Gilbert
2019-07-03
Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)
Gaëtan Gilbert
2019-07-02
[declare] Cleanup on imports, move exception.
Emilio Jesus Gallego Arias
2019-07-01
[declare] Remove superfluous API
Emilio Jesus Gallego Arias
2019-07-01
[declare] Separate kinds from entries in constant declaration
Emilio Jesus Gallego Arias
2019-07-01
[dumpglob] Move dumpglob-specific data to dumpglob.
Emilio Jesus Gallego Arias
2019-07-01
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
2019-06-27
Kernel transparent definition entries have no body universes.
Gaëtan Gilbert
2019-06-26
Perform the opaque section variable inference outside of the kernel.
Pierre-Marie Pédrot
2019-06-25
Move the internal_flag type from Declare to Ind_tables.
Pierre-Marie Pédrot
2019-06-25
Remove the internal_flag argument from Declare API.
Pierre-Marie Pédrot
2019-06-24
Use named records instead of tuples where `polymorphic` used to be.
Gaëtan Gilbert
2019-06-24
[api] Remove `polymorphic` type alias, use labels instead.
Emilio Jesus Gallego Arias
2019-06-24
[api] Move `locality` from `library` to `vernac`.
Emilio Jesus Gallego Arias
2019-06-24
Remove the export_seff flag from Declare API.
Pierre-Marie Pédrot
2019-06-24
Remove the unused opaque_entry_inline_code field from opaque entries.
Pierre-Marie Pédrot
2019-06-24
Enforce that opaque entries carry their type.
Pierre-Marie Pédrot
2019-06-24
Dedicated type for opaque entries in the kernel.
Pierre-Marie Pédrot
2019-06-24
Enforce that transparent entries are forced beforehand.
Pierre-Marie Pédrot
2019-06-24
Take advantage of the change of entry representation to split opacity status.
Pierre-Marie Pédrot
2019-06-24
Duplicate the type of constant entries in Proof_global.
Pierre-Marie Pédrot
2019-06-24
Move Declare to tactics folder.
Pierre-Marie Pédrot
[prev]
