diff --git a/_CoqProject b/_CoqProject
index a541dec3..f61e0c80 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -32,5 +32,6 @@ example_typed_store.v
 smallstep.v
 example_transformer.v
 category_ext.v
+all_monae.v
 
 -R . monae
diff --git a/all_monae.v b/all_monae.v
new file mode 100644
index 00000000..eaf670ee
--- /dev/null
+++ b/all_monae.v
@@ -0,0 +1,18 @@
+Require Export monae_lib.
+Require Export hierarchy.
+Require Export monad_lib.
+Require Export fail_lib.
+Require Export state_lib.
+Require Export array_lib.
+Require Export trace_lib.
+Require Export proba_lib.
+Require Export typed_store_lib.
+Require Export monad_composition.
+Require Export monad_model.
+Require Export proba_monad_model.
+Require Export category.
+Require Export gcm_model.
+Require Export altprob_model.
+Require Export monad_transformer.
+Require Export typed_store_model.
+Require Export category_ext.
diff --git a/hier.png b/hier.png
index 26e98f63..04a7978c 100644
Binary files a/hier.png and b/hier.png differ