diff --git a/.gitignore b/.gitignore
index f3d486137f42b4ddd2bf318827990b7ae63bb78d..cdc85f1dd8d62a02b8afed4b703afeecfadafd08 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,6 +18,7 @@ package.tgz
 .nia.cache
 .nra.cache
 .coqdeps.d
+.Makefile.d
 makefile
 Makefile
 makefile.bak
diff --git a/metrics.txt b/metrics.txt
new file mode 100644
index 0000000000000000000000000000000000000000..1e456d16ac9e4ad17390b6c41cb1fd1f7561b63d
--- /dev/null
+++ b/metrics.txt
@@ -0,0 +1,34 @@
+Formalization                              LOC (coqwc on spec + proof)
+===============================================
+Util
++-- Coqlib & Co                           2385
++-- FSets + FMaps                         4033
++-- MMultiset                             5807
+Core                                      1000
+Spaces
++-- Continuous spaces (R, R^2, etc.)      4490
++-- Discrete spaces (graphs, ring, grid)   686
+Observations
++-- Multiset                               293
++-- Set                                    265
++-- Other                                   68
+Models
++-- Rigid/flexible + equivalence           275
++-- Continuous/discrete graphs            1187
+Case Studies
++-- Gathering
+    +-- common part                       1407
+    +-- Impossibility (R + general)       2029
+    +-- SSYNC, R                          1388
+    +-- SSYNC, R^2                        2307
+    +-- Peleg + flexible                  1293
+    +-- Viglietta                          407
++-- Convergence
+    +-- Impossibility                      578
+    +-- Algorithm                          170
++-- Exploration
+    +-- Impossibility                      474
+    +-- Tower                              203
++-- Life-line                             1592
+===============================================
+Total                                    31462