coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of dev/doc/changes.md

July 2025

coqbot-app[bot]
Merge PR #20845: Rename repo references
committed
zimmi48.tngl.sh
Substitute all URLs to renamed repository.
committed

November 2023

coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed

October 2023

coqbot-app[bot]
Merge PR #18219: Typo fixed in changes.md
committed
Khalid Abdullah
Typo fixed in changes.md
committed

June 2023

coqbot-app[bot]
Merge PR #17382: [xml protocol] [coqide] Alternative PR fixing some loc problems in master.
committed
Emilio Jesus Gallego Arias
[xml protocol] Changelog and correct outdated documentation.
committed
coqbot-app[bot]
Merge PR #17117: Clarifying the logic of levels in custom and constr entry rules (reopening of #13025)
committed

May 2023

Hugo Herbelin
We introduce a type notation_entry_relative_level to preserve more informations about the subentries: we remember whether we are at any level, at the next level or at the self level.
committed

September 2022

coqbot-app[bot]
Merge PR #16567: Document the Subgoals XML command
committed
whonore
Document the Subgoals XML command
committed

June 2022

coqbot-app[bot]
Merge PR #16250: Remove some old scripts
committed
Gaëtan Gilbert
Remove some old scripts
committed
coqbot-app[bot]
Merge PR #16137: Improve dev changelog
committed
Théo Zimmermann
Add hint about what build system generates the META file.
committed
Théo Zimmermann
Fix typo in dev/doc/changes.
committed

May 2022

coqbot-app[bot]
Merge PR #15991: [mltop] Fix bug storing legacy module info in Summary
committed
Emilio Jesus Gallego Arias
[mltop] Improve and fix the legacy plugin loading method.
committed

November 2021

coqbot-app[bot]
Merge PR #15200: Describe changes from #14644 (Ltac visual debugger)
committed
Jim Fehrle
Describe changes from #14644 (Ltac visual debugger)
committed
coqbot-app[bot]
Merge PR #14644: Debugger part 3: display call stack and variable values
committed
Jim Fehrle
Send stack and variable maps through Answer, document protocol
committed

September 2021

coqbot-app[bot]
Merge PR #14846: Using the name of inductive types in inductive blocks rather than indices
committed
Hugo Herbelin
Pre-instantiate inductive types in the types of constructors.
committed
coqbot-app[bot]
Merge PR #14897: [changes] Rectify changelog w.r.t. configure fixes.
committed
Emilio Jesus Gallego Arias
[changes] Rectify changelog w.r.t. configure fixes.
committed
coqbot-app[bot]
Merge PR #14059: [build] [tools] Consolidation of directory handling code
committed
coqbot-app[bot]
Merge PR #12425: [ci] [gh-actions] Run the platform job using Github Actions
committed
Emilio Jesus Gallego Arias
[ci] [doc] Update documentation for the Gitlab actions platform PR
committed
Emilio Jesus Gallego Arias
[build] [tools] Consolidation of directory handling code
committed
Pierre-Marie Pédrot
Merge PR #14794: Adding a few functions about rel context in constr and econstr together with a reorganization
committed

August 2021

Hugo Herbelin
Documenting changes about functions on contexts.
committed
Pierre-Marie Pédrot
Merge PR #14598: Explicit Projection nodes in concrete syntax
committed
Hugo Herbelin
Update dev/doc/changes.md
committed
Hugo Herbelin
Update dev/doc/changes.md
committed

July 2021

Hugo Herbelin
Introducing specific constructors for projections in constr_expr, glob_term.
committed
coqbot-app[bot]
Merge PR #14654: A few terminology changes in module names of the universe API
committed
Hugo Herbelin
Renaming module LSet into Level.Set and LMap into Level.Map.
committed
Hugo Herbelin
Renaming module Univ.Constraint into Univ.Constraints.
committed
coqbot-app[bot]
Merge PR #14692: Embedding user-side universes names in Univ.UContext
committed
Hugo Herbelin
Simplifying code by embedding names in Univ.UContext.
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed
coqbot-app[bot]
Merge PR #14250: Split level creation from level population in Grammar
committed
Pierre-Marie Pédrot
Document the changes in the Gramlib API.
committed

April 2021

coqbot-app[bot]
Merge PR #14176: [build] Remove `-local` build layout, use always install-like layout
committed
Emilio Jesus Gallego Arias
[build] Remove `-local` build layout, use always install-like layout
committed
coqbot-app[bot]
Merge PR #13617: [build] Use dune to build OCaml code.
committed
Emilio Jesus Gallego Arias
[build] Use dune to build OCaml code.
committed
Pierre-Marie Pédrot
Merge PR #14075: New level of abstraction for streams with (non-canonical) location function
committed