index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
declare.mli
Age
Commit message (
Expand
)
Author
2020-04-21
[declare] [tactics] Move declare to `vernac`
Emilio Jesus Gallego Arias
2020-04-15
[tmp] Compat API for CI
Emilio Jesus Gallego Arias
2020-04-15
[declare] Rename `Declare.t` to `Declare.Proof.t`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Move functions related to `Proof.t` to `Proof`
Emilio Jesus Gallego Arias
2020-04-15
[declare] [abstract] Do evars check in declare_abstract
Emilio Jesus Gallego Arias
2020-04-15
[declare] Mark APIs as scheduled for removal; remove a couple.
Emilio Jesus Gallego Arias
2020-04-15
[proof] [abstract] Move internal declaration code to `Declare`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-03-31
[proof] Improve comment and argument name.
Emilio Jesus Gallego Arias
2020-03-31
[proof] Split delayed and regular proof closing functions, part II
Emilio Jesus Gallego Arias
2020-03-19
[declare] Remaining bits on the consistency of UState.t naming
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-12-22
Remove the hacks relying on hardwired libobject tags.
Pierre-Marie Pédrot
2019-10-30
[declare] Remove declare_scheme hook in Declare
Emilio Jesus Gallego Arias
2019-10-30
Merge PR #10949: [declare] Provide helper for private constant inlining.
Pierre-Marie Pédrot
2019-10-29
[declare] Use helper function for `fix_exn` instead of relying on internals.
Emilio Jesus Gallego Arias
2019-10-29
[declare] Make `proof_entry` a private type.
Emilio Jesus Gallego Arias
2019-10-28
[declare] Provide helper for private constant inlining.
Emilio Jesus Gallego Arias
2019-10-24
[declare] Split inductive declaration code to vernac/
Emilio Jesus Gallego Arias
2019-10-24
[declare] Split universe declaration code to vernac/
Emilio Jesus Gallego Arias
2019-10-16
Split the function used to declare side-effects from the standard one.
Pierre-Marie Pédrot
2019-10-13
Merge PR #10670: ComAssumption cleanup
Pierre-Marie Pédrot
2019-10-05
Declare universes for variables outside of Declare.declare_variable
Gaëtan Gilbert
2019-10-04
Remove redundancy in section hypotheses of kernel entries.
Pierre-Marie Pédrot
2019-08-27
[declare] Move proof_entry type to declare, put interactive proof data on top...
Emilio Jesus Gallego Arias
2019-08-19
[declare] Use `binding_kind` for implicit kind instead of boolean.
Emilio Jesus Gallego Arias
2019-07-03
declare_variable: path is always Lib.cwd()
Gaëtan Gilbert
2019-07-03
Declare section variables in direct style "without" an object
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
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
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
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
