diff --git a/dev/tools/mktoc b/dev/tools/mktoc
new file mode 100755
index 00000000..6d6c7eed
--- /dev/null
+++ b/dev/tools/mktoc
@@ -0,0 +1,118 @@
+#!/bin/sh
+
+usage()
+{
+	cat <<EOF
+Usage: mktoc FILE...
+Number sections, subsections and subsubsections in coqdoc'ed documented
+Coq FILEs.
+Also write a Table of content after a line
+*** Table of content
+if it is present in the file.
+The section, subsection and subsubsections have the following format:
+(** ** A section *)
+(** *** A subsection *)
+(** **** A subsubsection *)
+
+It is possible to reuse mktoc on the same file (e.g. to update the numbering and
+table of content after some changes).
+EOF
+}
+
+case $0 in
+0)
+	usage
+	exit 1
+esac
+
+case $1 in
+-h | --help)
+	usage
+	exit 0
+esac
+
+tmptoc=tmptoc$$.tmp
+tmpfile=tmp_mktoc_$$.tmp
+TOCSTRING='\\*\\*\\* Table of content'
+
+trap "rm -vf $tmptoc $tmpfile" EXIT SIGINT SIGTERM SIGABRT
+
+for f; do
+	# First pass to get the numbering right and write the TOC in a temporary file
+	>"$tmptoc"
+	awk -v "tmp=$tmptoc" '
+		function spaces(num_spaces) {
+			res = "";
+			for (i = 0; i < num_spaces; i++)
+				res = " " res;
+			return res;
+		}
+		function remove_numbering() {
+			if ($3 ~ /^[0-9.]+$/)
+				$3 = "";
+			gsub(/[[:blank:]]+/, " ");
+		}
+		BEGIN {
+			nb_levels = 0;
+		}
+		/^\(\*\*[[:blank:]]+\*\*+/ {
+			remove_numbering()
+
+			level = length($2) - 1;
+			if (level > nb_levels)
+				nb_levels = level
+
+			numbering[level - 1]++;
+			for (i = level; i < nb_levels; i++)
+				numbering[i] = 0
+			
+			title = $3;
+			for (i = 4; i < NF; i++)
+				title = title " " $i
+
+			if (level == 1) {
+				item = numbering[level - 1] ".";
+			} else {
+				item = numbering[0];
+				for (i = 1; i < level; i++)
+					item = item "." numbering[i]
+			}
+
+			printf("(** %s %s %s *)\n", $2, item, title);
+			printf("%s- %s %s\n", spaces(2 * (level - 1)), item, title) >>tmp
+			next
+		}
+		1
+	' <"$f" >"$tmpfile"
+
+	mv "$tmpfile" "$f"
+
+	# Second pass to write the TOC
+	awk -v "tmp=$tmptoc" -v "tocstring=$TOCSTRING" '
+		function spaces(num_spaces) {
+			res = "";
+			for (i = 0; i < num_spaces; i++)
+				res = " " res;
+			return res;
+		}
+		$0 ~ tocstring {
+			# we need to save the indentation level
+			match($0, /^ */);
+			indent = RLENGTH;
+			print $0;
+			# next line(s) should be empty, we also skip any previous TOC
+			do {
+				getline
+			} while ($0 ~ /^ *$/ || $0 ~ /^ *- [0-9][0-9.]+/);
+			# now we need to dump the new TOC
+			printf("\n");
+			while (getline line <tmp) {
+				printf("%s%s\n", spaces(indent), line)
+			}
+			printf("\n");
+		}
+		1
+	' <"$f" >"$tmpfile"
+
+	mv "$tmpfile" "$f"
+done
diff --git a/dev/tools/test/Makefile b/dev/tools/test/Makefile
new file mode 100644
index 00000000..7f77f412
--- /dev/null
+++ b/dev/tools/test/Makefile
@@ -0,0 +1,14 @@
+all: test-mkdoc
+
+test-mkdoc:
+	if [ -d mktoc/out ]; then rm -r mktoc/out; fi
+	mkdir mktoc/out
+	cp mktoc/example1.v mktoc/example2.v mktoc/out
+	../mktoc mktoc/out/example1.v mktoc/out/example2.v
+	@diff mktoc/out/example1.v mktoc/expected/example1.v || \
+		printf "test-mkdoc example1.v FAILED\n" 1>&2 && \
+		printf "test-mkdoc example1.v SUCCEEDED\n" 1>&2
+	@diff mktoc/out/example2.v mktoc/expected/example2.v || \
+		printf "test-mkdoc example2.v FAILED\n" 1>&2 && \
+		printf "test-mkdoc example2.v SUCCEEDED\n" 1>&2
+	rm -r mktoc/out
diff --git a/dev/tools/test/mktoc/example1.v b/dev/tools/test/mktoc/example1.v
new file mode 100644
index 00000000..92bb86ba
--- /dev/null
+++ b/dev/tools/test/mktoc/example1.v
@@ -0,0 +1,83 @@
+(** * Test file 1 for mktoc
+
+    *** Table of content
+    
+    Here is some random text we hope will remain after mktoc.
+
+    *** Some other part of this tutorial's header
+*)
+
+(** In this tutorial, we are going to search for lemmas, mostly about natural
+    numbers.
+
+    We already have all lemmas and definitions from the prelude ([Coq.Init]),
+    and we require the library file [Coq.Arith.PeanoNat] which adds hundreds
+    of new constants.
+*)
+
+From Coq Require Import PeanoNat.
+
+(** ** 42. Basic [Search] queries *)
+
+(** In its most basic form, one searches for lemmas or definitions containing
+   - a given constant, eg [Nat.add], or [nat]
+   - a given string to be part of the identifier
+   - a given notation
+*)
+
+(** Search all lemmas where the type [nat] and the operators (_ * _) and
+   (_ + _) occur. *)
+Search nat (_ + _) (_ * _). (* still too much *)
+
+(** ** 3.3.5 More sophisticated patterns *)
+
+(** Some text *)
+
+(** ** Filter results by logical kind and or syntax in queries *)
+
+(** We can also [Search] for a constant defined with a specific keyword.
+    For instance, the following lists all [Lemma]s whose names contain "add"
+    and types contain [0]: *)
+Search "add" 0 is:Lemma.
+
+(** ** 10.1 Disambiguating strings in Search queries *)
+
+(** ***  Some subsection *)
+
+(** **** 2 Some subsubsection *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** 42 Another one *)
+
+(** or, search for constants whose type contain a notation, such as: *)
+Search "||".
+Search "+".
+
+(** *** A Great subsection *)
+
+(** **** A subsubsection ! *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** Another subsubsection *)
+
+(** With some text inside *)
+
+(** **** Yet another subsubsection *)
+
+(** So, what really happens here?
+   Blah, blah, ... *)
+
+(** ** Searching for constants with given hypotheses (parameters) or conclusions (return type) *)
+
+(** Finally the [head] keyword is just a shorthand for [headconcl] or [headhyp]: *)
+Search head:"<->".
+
+(** ** 0.0.0 Searching inside or outside a specific module *)
+
+(** We hope mktoc works. *)
diff --git a/dev/tools/test/mktoc/example2.v b/dev/tools/test/mktoc/example2.v
new file mode 100644
index 00000000..53243a36
--- /dev/null
+++ b/dev/tools/test/mktoc/example2.v
@@ -0,0 +1,88 @@
+(** * Test file 1 for mktoc with a garbage TOC to remove
+
+    *** Table of content
+    
+    - 1. This
+      - 1.1 That
+      - 1.2 One
+    - 2. A
+      - 2.1 B
+      - 2.2 C
+
+    *** Some other part of this tutorial's header
+*)
+
+(** In this tutorial, we are going to search for lemmas, mostly about natural
+    numbers.
+
+    We already have all lemmas and definitions from the prelude ([Coq.Init]),
+    and we require the library file [Coq.Arith.PeanoNat] which adds hundreds
+    of new constants.
+*)
+
+From Coq Require Import PeanoNat.
+
+(** ** 42. Basic [Search] queries *)
+
+(** In its most basic form, one searches for lemmas or definitions containing
+   - a given constant, eg [Nat.add], or [nat]
+   - a given string to be part of the identifier
+   - a given notation
+*)
+
+(** Search all lemmas where the type [nat] and the operators (_ * _) and
+   (_ + _) occur. *)
+Search nat (_ + _) (_ * _). (* still too much *)
+
+(** ** 3.3.5 More sophisticated patterns *)
+
+(** Some text *)
+
+(** ** Filter results by logical kind and or syntax in queries *)
+
+(** We can also [Search] for a constant defined with a specific keyword.
+    For instance, the following lists all [Lemma]s whose names contain "add"
+    and types contain [0]: *)
+Search "add" 0 is:Lemma.
+
+(** ** 10.1 Disambiguating strings in Search queries *)
+
+(** ***  Some subsection *)
+
+(** **** 2 Some subsubsection *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** 42 Another one *)
+
+(** or, search for constants whose type contain a notation, such as: *)
+Search "||".
+Search "+".
+
+(** *** A Great subsection *)
+
+(** **** A subsubsection ! *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** Another subsubsection *)
+
+(** With some text inside *)
+
+(** **** Yet another subsubsection *)
+
+(** So, what really happens here?
+   Blah, blah, ... *)
+
+(** ** Searching for constants with given hypotheses (parameters) or conclusions (return type) *)
+
+(** Finally the [head] keyword is just a shorthand for [headconcl] or [headhyp]: *)
+Search head:"<->".
+
+(** ** 0.0.0 Searching inside or outside a specific module *)
+
+(** We hope mktoc works. *)
diff --git a/dev/tools/test/mktoc/expected/example1.v b/dev/tools/test/mktoc/expected/example1.v
new file mode 100644
index 00000000..b82713bf
--- /dev/null
+++ b/dev/tools/test/mktoc/expected/example1.v
@@ -0,0 +1,97 @@
+(** * Test file 1 for mktoc
+
+    *** Table of content
+
+    - 1. Basic [Search] queries
+    - 2. More sophisticated patterns
+    - 3. Filter results by logical kind and or syntax in queries
+    - 4. Disambiguating strings in Search queries
+      - 4.1 Some subsection
+        - 4.1.1 Some subsubsection
+        - 4.1.2 Another one
+      - 4.2 A Great subsection
+        - 4.2.1 A subsubsection !
+        - 4.2.2 Another subsubsection
+        - 4.2.3 Yet another subsubsection
+    - 5. Searching for constants with given hypotheses (parameters) or conclusions (return type)
+    - 6. Searching inside or outside a specific module
+
+    Here is some random text we hope will remain after mktoc.
+
+    *** Some other part of this tutorial's header
+*)
+
+(** In this tutorial, we are going to search for lemmas, mostly about natural
+    numbers.
+
+    We already have all lemmas and definitions from the prelude ([Coq.Init]),
+    and we require the library file [Coq.Arith.PeanoNat] which adds hundreds
+    of new constants.
+*)
+
+From Coq Require Import PeanoNat.
+
+(** ** 1. Basic [Search] queries *)
+
+(** In its most basic form, one searches for lemmas or definitions containing
+   - a given constant, eg [Nat.add], or [nat]
+   - a given string to be part of the identifier
+   - a given notation
+*)
+
+(** Search all lemmas where the type [nat] and the operators (_ * _) and
+   (_ + _) occur. *)
+Search nat (_ + _) (_ * _). (* still too much *)
+
+(** ** 2. More sophisticated patterns *)
+
+(** Some text *)
+
+(** ** 3. Filter results by logical kind and or syntax in queries *)
+
+(** We can also [Search] for a constant defined with a specific keyword.
+    For instance, the following lists all [Lemma]s whose names contain "add"
+    and types contain [0]: *)
+Search "add" 0 is:Lemma.
+
+(** ** 4. Disambiguating strings in Search queries *)
+
+(** *** 4.1 Some subsection *)
+
+(** **** 4.1.1 Some subsubsection *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** 4.1.2 Another one *)
+
+(** or, search for constants whose type contain a notation, such as: *)
+Search "||".
+Search "+".
+
+(** *** 4.2 A Great subsection *)
+
+(** **** 4.2.1 A subsubsection ! *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** 4.2.2 Another subsubsection *)
+
+(** With some text inside *)
+
+(** **** 4.2.3 Yet another subsubsection *)
+
+(** So, what really happens here?
+   Blah, blah, ... *)
+
+(** ** 5. Searching for constants with given hypotheses (parameters) or conclusions (return type) *)
+
+(** Finally the [head] keyword is just a shorthand for [headconcl] or [headhyp]: *)
+Search head:"<->".
+
+(** ** 6. Searching inside or outside a specific module *)
+
+(** We hope mktoc works. *)
diff --git a/dev/tools/test/mktoc/expected/example2.v b/dev/tools/test/mktoc/expected/example2.v
new file mode 100644
index 00000000..38ed5841
--- /dev/null
+++ b/dev/tools/test/mktoc/expected/example2.v
@@ -0,0 +1,95 @@
+(** * Test file 1 for mktoc with a garbage TOC to remove
+
+    *** Table of content
+
+    - 1. Basic [Search] queries
+    - 2. More sophisticated patterns
+    - 3. Filter results by logical kind and or syntax in queries
+    - 4. Disambiguating strings in Search queries
+      - 4.1 Some subsection
+        - 4.1.1 Some subsubsection
+        - 4.1.2 Another one
+      - 4.2 A Great subsection
+        - 4.2.1 A subsubsection !
+        - 4.2.2 Another subsubsection
+        - 4.2.3 Yet another subsubsection
+    - 5. Searching for constants with given hypotheses (parameters) or conclusions (return type)
+    - 6. Searching inside or outside a specific module
+
+    *** Some other part of this tutorial's header
+*)
+
+(** In this tutorial, we are going to search for lemmas, mostly about natural
+    numbers.
+
+    We already have all lemmas and definitions from the prelude ([Coq.Init]),
+    and we require the library file [Coq.Arith.PeanoNat] which adds hundreds
+    of new constants.
+*)
+
+From Coq Require Import PeanoNat.
+
+(** ** 1. Basic [Search] queries *)
+
+(** In its most basic form, one searches for lemmas or definitions containing
+   - a given constant, eg [Nat.add], or [nat]
+   - a given string to be part of the identifier
+   - a given notation
+*)
+
+(** Search all lemmas where the type [nat] and the operators (_ * _) and
+   (_ + _) occur. *)
+Search nat (_ + _) (_ * _). (* still too much *)
+
+(** ** 2. More sophisticated patterns *)
+
+(** Some text *)
+
+(** ** 3. Filter results by logical kind and or syntax in queries *)
+
+(** We can also [Search] for a constant defined with a specific keyword.
+    For instance, the following lists all [Lemma]s whose names contain "add"
+    and types contain [0]: *)
+Search "add" 0 is:Lemma.
+
+(** ** 4. Disambiguating strings in Search queries *)
+
+(** *** 4.1 Some subsection *)
+
+(** **** 4.1.1 Some subsubsection *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** 4.1.2 Another one *)
+
+(** or, search for constants whose type contain a notation, such as: *)
+Search "||".
+Search "+".
+
+(** *** 4.2 A Great subsection *)
+
+(** **** 4.2.1 A subsubsection ! *)
+
+(** We have seen two different usages of strings in search queries, namely,
+    searching for constants whose name contains the string, such as: *)
+Search "comm".
+
+(** **** 4.2.2 Another subsubsection *)
+
+(** With some text inside *)
+
+(** **** 4.2.3 Yet another subsubsection *)
+
+(** So, what really happens here?
+   Blah, blah, ... *)
+
+(** ** 5. Searching for constants with given hypotheses (parameters) or conclusions (return type) *)
+
+(** Finally the [head] keyword is just a shorthand for [headconcl] or [headhyp]: *)
+Search head:"<->".
+
+(** ** 6. Searching inside or outside a specific module *)
+
+(** We hope mktoc works. *)