index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
plugin_tutorial
/
tuto1
Age
Commit message (
Expand
)
Author
2020-06-26
[declare] Move proof information to declare.
Emilio Jesus Gallego Arias
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-04-16
Merge PR #11861: [declare] [rewrite] Use high-level declare API
Pierre-Marie Pédrot
2020-04-15
[declare] Rename `Declare.t` to `Declare.Proof.t`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Move proof_global functionality to Proof_global from Pfedit
Emilio Jesus Gallego Arias
2020-03-31
[nit] [plugin_tuto] Remove empty function and use new API directly
Emilio Jesus Gallego Arias
2020-03-30
[declare] Fuse prepare and declare for the non-interactive path.
Emilio Jesus Gallego Arias
2020-03-30
[declareDef] More consistent handling of universe binders
Emilio Jesus Gallego Arias
2020-03-30
[declare] [obligations] Refactor preparation of obligation entry
Emilio Jesus Gallego Arias
2020-03-19
[declare] Bring more consistency to parameters using labels
Emilio Jesus Gallego Arias
2019-10-25
[declare] Generalize kind type on declareDef
Emilio Jesus Gallego Arias
2019-08-24
[dune] Migrate static Dune files to Dune 1.10
Emilio Jesus Gallego Arias
2019-07-08
[api] Deprecate GlobRef constructors.
Emilio Jesus Gallego Arias
2019-07-01
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
2019-06-24
[api] Move `locality` from `library` to `vernac`.
Emilio Jesus Gallego Arias
2019-06-24
[lemmas] [proof] Split proof kinds into per-layer components.
Emilio Jesus Gallego Arias
2019-06-17
Allow to delay polymorphic opaque constants.
Pierre-Marie Pédrot
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-08
Cleaning the status of Local Definition and similar.
Hugo Herbelin
2019-06-06
Clean, document, and expand plugin tutorials 0 and 1
Talia Ringer
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-06-03
Update tutorial plugin to use sigma, in keeping with doc recommendations
Talia Ringer
2019-05-24
Remove the indirect opaque accessor hooks from Opaqueproof.
Pierre-Marie Pédrot
2019-05-21
Remove definition-not-visible warning
Gaëtan Gilbert
2019-05-01
[comDefinition] Use prepare function from DeclareDef.
Emilio Jesus Gallego Arias
2019-03-27
[plugin tutorial] Adapt to removal of imperative state.
Emilio Jesus Gallego Arias
2019-02-23
[vernac] Unify declaration hooks.
Emilio Jesus Gallego Arias
2019-02-11
Fix #9527: unknown evar in nonterminating [fix] error.
Gaëtan Gilbert
2019-01-08
Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e...
Gaëtan Gilbert
