Best practice

1 files changed, 17 insertions, 0 deletions

diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md
new file mode 100644
index 0000000..ba15070
--- /dev/null
+++ b/src/BEST_PRACTICE.md
@@ -0,0 +1,17 @@
+# Proofs
+## Axioms
+
+No axiom should be added. No library adding axioms should be imported.
+
+
+# Code organization
+## Theories
+
+Theories are organized in sub-directories whose names are the names of
+each theory.
+
+
+## Compilation
+
+Before pushing or making a pull request to the master branch, make sure
+that the project compiles with both standard and native Coq.