From 16cb25a1660ed12c161ed73dd2eb5c571663121a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 11 May 2026 16:46:16 +0200
Subject: [PATCH] Add a Version file allowing to identify the stdlib library
 version from rocq.

---
 dev/doc/howto_release.md | 1 +
 theories/All.sh          | 4 +++-
 theories/Version.v       | 2 ++
 3 files changed, 6 insertions(+), 1 deletion(-)
 create mode 100644 theories/Version.v

diff --git a/dev/doc/howto_release.md b/dev/doc/howto_release.md
index aa1aa7a7aa..93ace5d631 100644
--- a/dev/doc/howto_release.md
+++ b/dev/doc/howto_release.md
@@ -1,6 +1,7 @@
 * generate changelog with dev/tools/generate-release-changelog.sh
   and update doc/sphinx/changes.rst accordingly
 * update doc/sphinx/conf.py (particularly is_a_released_version)
+* update theories/Version.v
 * check the result of "make refman-html"
   (in _build/default/doc/refman-html)
 * if need be, update supported versions of Rocq in .nix/config.nix
diff --git a/theories/All.sh b/theories/All.sh
index 7c6fcfb8a0..e5363de786 100755
--- a/theories/All.sh
+++ b/theories/All.sh
@@ -10,5 +10,7 @@ if [ "$1" = "-unsorted" ]; then
 else
   rocqdep="xargs rocq dep -Q . Stdlib -sort"
 fi
-find . -regex '.*/[^.][^/]*[.]v' ! -path ./All.v | sort | $rocqdep | \
+find . -regex '.*/[^.][^/]*[.]v' ! -path ./All.v ! -path ./Version.v | sort | $rocqdep | \
   sed -e 's#\./#From Stdlib Require Export #g' -e 's#\.v\s*#.\n#g' -e 's#/#.#g'
+
+printf 'From Stdlib Require Export Version.\n'
\ No newline at end of file
diff --git a/theories/Version.v b/theories/Version.v
new file mode 100644
index 0000000000..88ab2fdeef
--- /dev/null
+++ b/theories/Version.v
@@ -0,0 +1,2 @@
+From Corelib Require Import PrimString.
+Definition version : string := "9.2".
\ No newline at end of file