coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of doc/plugin_tutorial/tuto1/src/simple_declare.ml

November 2021

coqbot-app[bot]
Merge PR #15233: Reduce explicit use of default definition scope
committed
Gaëtan Gilbert
Reduce explicit use of default definition scope
committed

June 2020

Gaëtan Gilbert
Merge PR #12372: [declare] Refactor constant information into a record.
committed
Emilio Jesus Gallego Arias
[declare] Improve organization of proof/constant information.
committed
Emilio Jesus Gallego Arias
[declare] [api] Removal of duplicated type aliases.
committed
Emilio Jesus Gallego Arias
[declare] Refactor constant information into a record.
committed

May 2020

Gaëtan Gilbert
Merge PR #12241: [declare] Merge DeclareDef into Declare
committed
Emilio Jesus Gallego Arias
[declare] Merge DeclareDef into Declare
committed

April 2020

Pierre-Marie Pédrot
Merge PR #11861: [declare] [rewrite] Use high-level declare API
committed

March 2020

Emilio Jesus Gallego Arias
[nit] [plugin_tuto] Remove empty function and use new API directly
committed
Gaëtan Gilbert
Merge PR #11818: [proof] Further consolidation of the regular declaration path
committed
Emilio Jesus Gallego Arias
[declare] Fuse prepare and declare for the non-interactive path.
committed
Emilio Jesus Gallego Arias
[declareDef] More consistent handling of universe binders
committed
Emilio Jesus Gallego Arias
[declare] [obligations] Refactor preparation of obligation entry
committed
Gaëtan Gilbert
Merge PR #11731: [proof] Miscellaneous refactorings
committed
Emilio Jesus Gallego Arias
[declare] Bring more consistency to parameters using labels
committed

October 2019

Gaëtan Gilbert
Merge PR #10516: [funind] Remove duplicate save function.
committed
Emilio Jesus Gallego Arias
[declare] Generalize kind type on declareDef
committed

July 2019

Gaëtan Gilbert
Merge PR #10419: [api] Refactor most of `Decl_kinds`
committed
Emilio Jesus Gallego Arias
[api] Refactor most of `Decl_kinds`
committed

June 2019

Pierre-Marie Pédrot
Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.
committed
Emilio Jesus Gallego Arias
[api] Move `locality` from `library` to `vernac`.
committed
Emilio Jesus Gallego Arias
[lemmas] [proof] Split proof kinds into per-layer components.
committed
Pierre-Marie Pédrot
Merge PR #8726: More robust treatment of the Discharge status
committed
Hugo Herbelin
Cleaning the status of Local Definition and similar.
committed
Pierre-Marie Pédrot
Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain more
committed
Talia Ringer
Clean, document, and expand plugin tutorials 0 and 1
committed

May 2019

Talia Ringer
Merge remote-tracking branch 'origin/master' into stm+doc_hook
committed
Emilio Jesus Gallego Arias
Merge PR #10188: Remove definition-not-visible warning
committed
Gaëtan Gilbert
Remove definition-not-visible warning
committed
Gaëtan Gilbert
Merge PR #10038: [comDefinition] Use prepare function from DeclareDef.
committed
Emilio Jesus Gallego Arias
[comDefinition] Use prepare function from DeclareDef.
committed

March 2019

Maxime Dénès
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.
committed
Emilio Jesus Gallego Arias
[plugin tutorial] Adapt to removal of imperative state.
committed

February 2019

Maxime Dénès
Merge PR #9567: [vernac] Unify declaration hooks.
committed
Emilio Jesus Gallego Arias
[vernac] Unify declaration hooks.
committed

January 2019

Yves Bertot
Merge pull request #8778 from SkySkimmer/merge-plugin-tuto
committed
Gaëtan Gilbert
Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'
committed