aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/src
AgeCommit message (Expand)Author
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-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 PfeditEmilio Jesus Gallego Arias
2020-03-31[nit] [plugin_tuto] Remove empty function and use new API directlyEmilio 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 bindersEmilio Jesus Gallego Arias
2020-03-30[declare] [obligations] Refactor preparation of obligation entryEmilio Jesus Gallego Arias
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2019-10-25[declare] Generalize kind type on declareDefEmilio Jesus Gallego Arias
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio 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-17Allow 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-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-06-03Update tutorial plugin to use sigma, in keeping with doc recommendationsTalia Ringer
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-21Remove definition-not-visible warningGaë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-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-01-08Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e...Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:51:31 +0000