coq
forked from coq/coq
Star 1
Fork 0
Watch

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

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

October 2024

coqbot-app[bot]
Merge PR #19743: Rocqify Coqlib
committed
Pierre-Marie Pédrot
Rename the Coqlib module into Rocqlib.
committed

April 2024

coqbot-app[bot]
Merge PR #18938: Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
Gaëtan Gilbert
Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
coqbot-app[bot]
Merge PR #18868: Move from deprecated find_reference to lib_ref in the plugin tutorial
committed

March 2024

Julien Puydt
Move from deprecated find_reference to lib_ref in the plugin tutorial
committed

January 2022

coqbot-app[bot]
Merge PR #15414: Reduce the use of `Global` functions
committed

December 2021

Pierre-Marie Pédrot
Remove calls to Global functions in the plugin tutorial.
committed

October 2021

coqbot-app[bot]
Merge PR #15069: Remove most calls to Global from engine/
committed
Pierre-Marie Pédrot
Remove Evarutil.new_global.
committed
Pierre-Marie Pédrot
Remove the easy call to Global.env from Evarutil.
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