diff --git a/extra-dev/packages/coq-bits/coq-bits.dev/opam b/extra-dev/packages/coq-bits/coq-bits.dev/opam
new file mode 100644
index 000000000..6c062cc72
--- /dev/null
+++ b/extra-dev/packages/coq-bits/coq-bits.dev/opam
@@ -0,0 +1,42 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "anton.a.trunov@gmail.com"
+
+homepage: "https://github.com/coq-community/bits"
+dev-repo: "git+https://github.com/coq-community/bits.git"
+bug-reports: "https://github.com/coq-community/bits/issues"
+license: "Apache-2.0"
+
+synopsis: "Coq bit vector library"
+description: """
+A formalization of bitset operations in Coq with a corresponding
+axiomatization and extraction to OCaml native integers."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "ocamlbuild" 
+  "coq-mathcomp-algebra" {= "dev"}
+  "coq-mathcomp-algebra-tactics"
+]
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "keyword:bit arithmetic"
+  "keyword:bitset"
+  "keyword:bit vector"
+  "keyword:extraction"
+  "logpath:Bits"
+]
+authors: [
+  "Andrew Kennedy <akenn@microsoft.com>"
+  "Arthur Blot <arthur.blot@ens-lyon.fr>"
+  "Pierre-Évariste Dagand <pierre-evariste.dagand@lip6.fr>"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/bits.git#master"
+}
diff --git a/extra-dev/packages/coq-cds4ltl/coq-cds4ltl.dev/opam b/extra-dev/packages/coq-cds4ltl/coq-cds4ltl.dev/opam
new file mode 100644
index 000000000..6e43ad464
--- /dev/null
+++ b/extra-dev/packages/coq-cds4ltl/coq-cds4ltl.dev/opam
@@ -0,0 +1,33 @@
+opam-version: "2.0"
+maintainer: "johnw@newartisans.com"
+
+homepage: "https://github.com/jwiegley/coq-cds4ltl"
+dev-repo: "git+https://github.com/jwiegley/coq-cds4ltl.git"
+bug-reports: "https://github.com/jwiegley/coq-cds4ltl/issues"
+license: "BSD-3-Clause"
+
+synopsis: "A Calculational Deductive System for Linear Temporal Logic"
+description: """
+An axiomatic and denotational formalization of the theorems described by the
+paper: A Calculational Deductive System for Linear Temporal Logic (CDS4LTL).
+"""
+
+build: [make "-j%{jobs}%" ]
+install: [make "install"]
+depends: [
+  "rocq-core" {= "dev"}
+  "rocq-stdlib" {= "dev"}
+]
+
+tags: [
+  "keyword: temporal logic"
+  "category: Mathematics/Logic/Modal logic"
+  "logpath: CDS4LTL"
+]
+authors: [
+  "John Wiegley"
+]
+
+url {
+  src: "git+https://github.com/jwiegley/coq-cds4ltl.git#master"
+}
diff --git a/extra-dev/packages/coq-comp-dec-modal/coq-comp-dec-modal.dev/opam b/extra-dev/packages/coq-comp-dec-modal/coq-comp-dec-modal.dev/opam
new file mode 100644
index 000000000..34a3a8b5f
--- /dev/null
+++ b/extra-dev/packages/coq-comp-dec-modal/coq-comp-dec-modal.dev/opam
@@ -0,0 +1,55 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "christian.doczkal@inria.fr"
+
+homepage: "https://github.com/coq-community/comp-dec-modal"
+dev-repo: "git+https://github.com/coq-community/comp-dec-modal.git"
+bug-reports: "https://github.com/coq-community/comp-dec-modal/issues"
+doc: "https://coq-community.github.io/comp-dec-modal/"
+license: "CECILL-B"
+
+synopsis: "Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse"
+description: """
+This project presents machine-checked constructive proofs of
+soundness, completeness, decidability, and the small-model property
+for the logics K, K*, CTL, and PDL (with and without converse).
+
+For all considered logics, we prove soundness and completeness of
+their respective Hilbert-style axiomatization. For K, K*, and CTL,
+we also prove soundness and completeness for Gentzen systems (i.e.,
+sequent calculi).
+
+For each logic, the central construction is a pruning-based
+algorithm computing for a given formula either a satisfying model of
+bounded size or a proof of its negation. The completeness and
+decidability results then follow with soundness from the existence
+of said algorithm.
+  """
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-hierarchy-builder" {>= "1.6.0"}
+]
+
+tags: [
+  "category:Mathematics/Logic/Modal logic"
+  "keyword:modal logic"
+  "keyword:completeness"
+  "keyword:decidability"
+  "keyword:Hilbert system"
+  "keyword:computation tree logic"
+  "keyword:propositional dynamic logic"
+  "logpath:CompDecModal"
+]
+authors: [
+  "Christian Doczkal"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/comp-dec-modal.git#master"
+}
diff --git a/extra-dev/packages/coq-coqtail/coq-coqtail.dev/opam b/extra-dev/packages/coq-coqtail/coq-coqtail.dev/opam
new file mode 100644
index 000000000..44efba791
--- /dev/null
+++ b/extra-dev/packages/coq-coqtail/coq-coqtail.dev/opam
@@ -0,0 +1,41 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/coqtail-math"
+dev-repo: "git+https://github.com/coq-community/coqtail-math.git"
+bug-reports: "https://github.com/coq-community/coqtail-math/issues"
+license: "LGPL-3.0-only"
+
+synopsis: "Library of mathematical theorems and tools proved inside the Coq"
+description: """
+Coqtail is a library of mathematical theorems and tools proved inside
+the Coq proof assistant. Results range mostly from arithmetic to real
+and complex analysis."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+]
+
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword:real analysis"
+  "keyword:complex analysis"
+  "logpath:Coqtail"
+]
+authors: [
+  "Guillaume Allais"
+  "Sylvain Dailler"
+  "Hugo Férée"
+  "Jean-Marie Madiot"
+  "Pierre-Marie Pédrot"
+  "Amaury Pouly"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/coqtail-math.git#master"
+}
diff --git a/extra-dev/packages/coq-exact-real-arithmetic/coq-exact-real-arithmetic.dev/opam b/extra-dev/packages/coq-exact-real-arithmetic/coq-exact-real-arithmetic.dev/opam
new file mode 100644
index 000000000..cb2eb4e29
--- /dev/null
+++ b/extra-dev/packages/coq-exact-real-arithmetic/coq-exact-real-arithmetic.dev/opam
@@ -0,0 +1,30 @@
+opam-version: "2.0"
+maintainer: "Hugo.Herbelin@inria.fr"
+homepage: "https://github.com/rocq-community/exact-real-arithmetic"
+license: "LGPL 2.1"
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "ocaml"
+  "coq" {= "dev"}
+]
+tags: [
+  "keyword: correctness"
+  "keyword: real numbers"
+  "keyword: arithmetic"
+  "category: Mathematics/Real Numbers"
+]
+authors: [
+  "Jérôme Creci"
+]
+bug-reports: "https://github.com/rocq-community/exact-real-arithmetic/issues"
+dev-repo: "git+https://github.com/rocq-community/exact-real-arithmetic.git"
+synopsis: "Exact Real Arithmetic"
+description: """
+This contribution contains a proof of correctness
+of some exact real arithmetic algorithms from the PhD thesis of
+Valérie Ménissier-Morain"""
+
+url {
+  src: "git+https://github.com/rocq-community/exact-real-arithmetic.git#master"
+}
diff --git a/extra-dev/packages/coq-hanoi/coq-hanoi.dev/opam b/extra-dev/packages/coq-hanoi/coq-hanoi.dev/opam
new file mode 100644
index 000000000..a9148194b
--- /dev/null
+++ b/extra-dev/packages/coq-hanoi/coq-hanoi.dev/opam
@@ -0,0 +1,59 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "thery@sophia.inria.fr"
+
+homepage: "https://github.com/thery/hanoi"
+dev-repo: "git+https://github.com/thery/hanoi.git"
+bug-reports: "https://github.com/thery/hanoi/issues"
+license: "MIT"
+
+synopsis: "Hanoi tower in Rocq"
+description: """
+Hanoi tower in Rocq
+
+
+| File                              |  Content                                 | 
+| --------------------------------- | -----------------------------------------| 
+| [extra](./extra.v)                | Extra theorems from the standard library |
+| [gdist](./gdist.v)                | Distance in a graph                      |
+| [ghanoi](./ghanoi.v)              | General Hanoi framework                  |
+| [ghanoi3](./ghanoi3.v)            | General Hanoi framework with 3 pegs      |
+| [lhanoi3](./lhanoi3.v)            | Linear Hanoi tower with 3 pegs           |
+| [rhanoi3](./rhanoi3.v)            | Regular Hanoi tower with 3 pegs          |
+| [triangular](./triangular.v)      | Theorems about triangular numbers        |
+| [phi](./phi.v)                    | Theorems about the Φ function            |
+| [psi](./psi.v)                    | Theorems about the Ψ function            |
+| [ghanoi4](./ghanoi4.v)            | General Hanoi framework with 4 pegs      |
+| [rhanoi4](./rhanoi4.v)            | Regular Hanoi tower with 4 pegs          |
+| [star](./star.v)                  | Some maths for the shanoi                |
+| [shanoi](./shanoi.v)              | Hanoi tower in star                      |
+| [shanoi4](./shanoi4.v)            | Hanoi tower with 4 pegs in star          |
+
+A note about this development is available 
+[here](https://hal.inria.fr/hal-02903548).
+
+An interactive version of the library is available 
+[here](https://thery.github.io/hanoi/index.html)."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "rocq-mathcomp-ssreflect" {(>= "2.5.0")}
+  "rocq-mathcomp-algebra" {(>= "2.5.0")}
+  "coq-mathcomp-finmap" {(>= "2.2.2")}
+]
+
+tags: [
+  "keyword:hanoi tower"
+  "logpath:hanoi"
+]
+authors: [
+  "Laurent Théry"
+]
+
+url {
+  src: "git+https://github.com/thery/hanoi.git#master"
+}
diff --git a/extra-dev/packages/coq-mathcomp-abel/coq-mathcomp-abel.dev/opam b/extra-dev/packages/coq-mathcomp-abel/coq-mathcomp-abel.dev/opam
new file mode 100644
index 000000000..42758c0e9
--- /dev/null
+++ b/extra-dev/packages/coq-mathcomp-abel/coq-mathcomp-abel.dev/opam
@@ -0,0 +1,48 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+
+homepage: "https://github.com/math-comp/abel"
+dev-repo: "git+https://github.com/math-comp/abel.git"
+bug-reports: "https://github.com/math-comp/abel/issues"
+license: "CECILL-B"
+
+synopsis: "Abel - Ruffini's theorem"
+description: """
+This repository contains a proof of Abel - Galois Theorem
+(equivalence between being solvable by radicals and having a
+solvable Galois group) and Abel - Ruffini Theorem (unsolvability of
+quintic equations) in the Coq proof-assistant and using the
+Mathematical Components library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "rocq-core" {= "dev"}
+  "coq-mathcomp-ssreflect" {= "dev"}
+  "coq-mathcomp-fingroup" 
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-solvable" 
+  "coq-mathcomp-field" 
+  "coq-mathcomp-real-closed" {= "dev"}
+]
+
+tags: [
+  "keyword:algebra"
+  "keyword:Galois"
+  "keyword:Abel Ruffini"
+  "keyword:unsolvability of quintincs"
+  "logpath:Abel"
+]
+authors: [
+  "Sophie Bernard"
+  "Cyril Cohen"
+  "Assia Mahboubi"
+  "Pierre-Yves Strub"
+]
+
+url {
+  src: "git+https://github.com/math-comp/abel.git#master"
+}
diff --git a/extra-dev/packages/coq-mathcomp-apery/coq-mathcomp-apery.dev/opam b/extra-dev/packages/coq-mathcomp-apery/coq-mathcomp-apery.dev/opam
new file mode 100644
index 000000000..2f5592739
--- /dev/null
+++ b/extra-dev/packages/coq-mathcomp-apery/coq-mathcomp-apery.dev/opam
@@ -0,0 +1,51 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "assia.mahboubi@inria.fr"
+
+homepage: "https://github.com/coq-community/apery"
+dev-repo: "git+https://github.com/coq-community/apery.git"
+bug-reports: "https://github.com/coq-community/apery/issues"
+license: "CECILL-C"
+
+synopsis: "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational"
+description: """
+This project contains a formal proof that the real number ζ(3),
+also known as Apéry's constant, is irrational. It follows roughly
+Apéry's original sketch of a proof. However, the recurrence
+relations constituting the crux of the proof have been guessed by a
+computer algebra program (in this case in Maple/Algolib). These
+relations are formally checked a posteriori, so that Coq's kernel
+remains the sole trusted code base."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "coq-mathcomp-ssreflect" {= "dev"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-field" 
+  "coq-coqeal" {>= "2.1.0"}
+  "coq-mathcomp-real-closed" {= "dev"}
+  "coq-mathcomp-bigenough" {= "dev"}
+  "coq-mathcomp-zify" 
+  "coq-mathcomp-algebra-tactics" 
+]
+
+tags: [
+  "category:Mathematics/Arithmetic and Number Theory/Number theory"
+  "keyword:apery recurrence"
+  "keyword:irrationality"
+  "keyword:creative telescoping"
+  "logpath:mathcomp.apery"
+]
+authors: [
+  "Frédéric Chyzak"
+  "Assia Mahboubi"
+  "Thomas Sibut-Pinote"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/apery.git#master"
+}
diff --git a/extra-dev/packages/coq-mmaps/coq-mmaps.dev/opam b/extra-dev/packages/coq-mmaps/coq-mmaps.dev/opam
new file mode 100644
index 000000000..91271e239
--- /dev/null
+++ b/extra-dev/packages/coq-mmaps/coq-mmaps.dev/opam
@@ -0,0 +1,41 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/coq-mmaps"
+dev-repo: "git+https://github.com/coq-community/coq-mmaps.git"
+bug-reports: "https://github.com/coq-community/coq-mmaps/issues"
+license: "LGPL-2.1-only"
+
+synopsis: "Several implementations of finite maps over arbitrary ordered types using Coq functors"
+description: """
+This project contains several implementations of finite maps,
+including implementations based on AVL trees and red-black trees.
+The finite maps are parameterized on arbitrary ordered types using
+Coq functors. This is an updated version of the Coq Stdlib's FMaps
+that is meant to complement the Stdlib's MSet library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+]
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "keyword:finite maps"
+  "keyword:red-black trees"
+  "keyword:AVL trees"
+  "keyword:ordered types"
+  "logpath:MMaps"
+]
+authors: [
+  "Pierre Letouzey"
+  "Andrew W. Appel"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/mmaps.git#master"
+}
diff --git a/extra-dev/packages/coq-stalmarck-tactic/coq-stalmarck-tactic.dev/opam b/extra-dev/packages/coq-stalmarck-tactic/coq-stalmarck-tactic.dev/opam
new file mode 100644
index 000000000..c616d9f0a
--- /dev/null
+++ b/extra-dev/packages/coq-stalmarck-tactic/coq-stalmarck-tactic.dev/opam
@@ -0,0 +1,34 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/stalmarck"
+dev-repo: "git+https://github.com/coq-community/stalmarck.git"
+bug-reports: "https://github.com/coq-community/stalmarck/issues"
+license: "LGPL-2.1-or-later"
+
+synopsis: "Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm"
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "ocaml" {>= "4.09.0"}
+  "dune" {>= "2.8" & < "3.24"}
+  "coq" {= "dev"}
+  "coq-stalmarck" {= version}
+]
+
+tags: [
+  "category:Miscellaneous/Coq Extensions"
+  "category:Miscellaneous/Extracted Programs/Decision procedures"
+  "keyword:boolean formula"
+  "keyword:tautology checker"
+  "keyword:tactics"
+  "logpath:Stalmarck.Tactic"
+]
+authors: [
+  "Pierre Letouzey"
+  "Laurent Théry"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/stalmarck.git#master"
+}
diff --git a/extra-dev/packages/coq-stalmarck/coq-stalmarck.dev/opam b/extra-dev/packages/coq-stalmarck/coq-stalmarck.dev/opam
new file mode 100644
index 000000000..462bd5099
--- /dev/null
+++ b/extra-dev/packages/coq-stalmarck/coq-stalmarck.dev/opam
@@ -0,0 +1,36 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/stalmarck"
+dev-repo: "git+https://github.com/coq-community/stalmarck.git"
+bug-reports: "https://github.com/coq-community/stalmarck/issues"
+license: "LGPL-2.1-or-later"
+
+synopsis: "Verified implementation of Stålmarck's algorithm for proving tautologies in Coq"
+description: """
+A two-level approach to prove tautologies using Stålmarck's
+algorithm in Coq."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+]
+
+tags: [
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "keyword:boolean formula"
+  "keyword:tautology checker"
+  "logpath:Stalmarck.Algorithm"
+]
+authors: [
+  "Pierre Letouzey"
+  "Laurent Théry"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/stalmarck.git#master"
+}
diff --git a/extra-dev/packages/coq-sum-of-two-square/coq-sum-of-two-square.dev/opam b/extra-dev/packages/coq-sum-of-two-square/coq-sum-of-two-square.dev/opam
new file mode 100644
index 000000000..3045f3322
--- /dev/null
+++ b/extra-dev/packages/coq-sum-of-two-square/coq-sum-of-two-square.dev/opam
@@ -0,0 +1,45 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "thery@sophia.inria.fr"
+
+homepage: "https://github.com/rocq-archive/sum-of-two-square"
+dev-repo: "git+https://github.com/rocq-archive/sum-of-two-square.git"
+bug-reports: "https://github.com/rocq-archive/sum-of-two-square/issues"
+license: "MIT"
+
+synopsis: "when a number n can be written as the sum of two square numbers"
+description: """
+
+This directory contains the proof that a number n can be written as the 
+sum of two square numbers if and only if each prime factor $p$ of $n$ 
+that is equal to 3 modulo 4 has its exponent in the decomposition of n
+that is even.
+
+A note on the development is available at [here](https://inria.hal.science/hal-05025371)
+
+
+To build the directory, type
+
+  make all
+
+Laurent Thery thery@sophia.inria.fr"""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+]
+
+tags: [
+  "keyword:sum two square"
+  "logpath:SumOfTwoSquare"
+]
+authors: [
+  "Laurent Théry"
+]
+
+url {
+  src: "git+https://github.com/rocq-archive/sum-of-two-square.git#master"
+}
diff --git a/extra-dev/packages/coq-waterproof/coq-waterproof.dev/opam b/extra-dev/packages/coq-waterproof/coq-waterproof.dev/opam
new file mode 100644
index 000000000..38d8bb11d
--- /dev/null
+++ b/extra-dev/packages/coq-waterproof/coq-waterproof.dev/opam
@@ -0,0 +1,47 @@
+opam-version: "2.0"
+name: "coq-waterproof"
+maintainer: "Jim Portegies <j.w.portegies@tue.nl>"
+authors: [
+  "Jelle Wemmenhove"
+  "Pim Otte"
+  "Balthazar Pathiachvili"
+  "Dick Arends"
+  "Cosmin Manea"
+  "Lulof Pirée"
+  "Adrian Vrămuleţ"
+  "Tudor Voicu"
+  "Jim Portegies <j.w.portegies@tue.nl>"
+]
+
+synopsis: "Coq proofs in a style that resembles non-mechanized mathematical proofs"
+description: """
+The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
+"""
+
+license: "LGPL-3.0-or-later"
+homepage: "https://github.com/impermeable/coq-waterproof"
+dev-repo: "git+https://github.com/impermeable/coq-waterproof.git"
+bug-reports: "https://github.com/impermeable/coq-waterproof/issues"
+
+depends: [
+  "ocaml" {>= "4.09.0"}
+  "coq" {= "dev"}
+  "dune" {>= "3.8" & < "3.24"}
+]
+
+build: [
+  ["dune" "build" "-p" name "-j" jobs "@install"]
+]
+
+available: (arch != "s390x") & (arch != "ppc64")
+
+tags: [
+  "keyword:mathematics education"
+  "category:Mathematics/Education"
+  "date:2023-11-04"
+  "logpath:Waterproof"
+]
+
+url {
+  src: "git+https://github.com/impermeable/coq-waterproof.git#coq-master"
+}