coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of doc/plugin_tutorial/tuto3/src/tuto_tactic.ml

June 2026

coqbot-app[bot]
Merge PR #21987: Keep track of which variables are section variables and use this info to fix bugs
committed

May 2026

Gaëtan Gilbert
Keep track of variable status (secvar or not) in named contexts
committed

November 2025

coqbot-app[bot]
Merge PR #21336: Clean Tacmach API
committed
Pierre-Marie Pédrot
Deprecate Tacmach.pf_concl.
committed
Pierre-Marie Pédrot
Deprecate Tacmach.project.
committed

March 2025

Pierre-Marie Pédrot
Put back the TC candidate optional, but now false by default.
committed
Pierre-Marie Pédrot
Stop relying on a hook to set the TC flag of freshly declared evars.
committed

December 2024

coqbot-app[bot]
Merge PR #19530: Give Stdlib its own directory
committed
Pierre Roux
Use Corelib instead of Stdlib as namespace for rocq-core
committed

October 2024

coqbot-app[bot]
Merge PR #19738: Remove deprecated coqlib API
committed
Pierre-Marie Pédrot
Replace some deprecated calls to Coqlib APIs by their modern variants.
committed

September 2024

coqbot-app[bot]
Merge PR #19310: Rename Coq requirement prefix to Stdlib
committed
Pierre Roux
Renaming Coq -> Stdlib
committed

November 2021

coqbot-app[bot]
Merge PR #15159: Make the new Tacmach/Tacticals API the default.
committed
Pierre-Marie Pédrot
Swap the role of the legacy and modern Tacmach layers.
committed

October 2021

coqbot-app[bot]
Merge PR #15069: Remove most calls to Global from engine/
committed
Pierre-Marie Pédrot
Remove some calls to Global functions in UnivGen.
committed

June 2019

Jim Fehrle
Merge branch 'master' of https://github.com/coq/coq
committed
Enrico Tassi
Merge PR #10287: Update tutorial plugin to use sigma instad of evd, in keeping with doc recommendations
committed
Talia Ringer
Update tutorial plugin to use sigma, in keeping with doc recommendations
committed

March 2019

Pierre-Marie Pédrot
Merge PR #8817: SProp: the definitionally proof irrelevant universe
committed
Gaëtan Gilbert
Add relevance marks on binders.
committed

January 2019

Yves Bertot
Merge pull request #8778 from SkySkimmer/merge-plugin-tuto
committed
Gaëtan Gilbert
plugin_tutorial: ignore Coqlib.find_reference deprecation warning.
committed
Gaëtan Gilbert
Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'
committed