aboutsummaryrefslogtreecommitdiffstats
path: root/src/BEST_PRACTICE.md
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2020-01-28 14:42:07 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2020-01-28 14:42:07 +0100
commita845071c6ab36da0cb8c82b17b461b4f2f0342f5 (patch)
treea2f870b414d64d067b149231a5b145ef0f96b65e /src/BEST_PRACTICE.md
parent53e71fe319df5319cd0451625e2ca039ad7b7cb2 (diff)
downloadsmtcoq-a845071c6ab36da0cb8c82b17b461b4f2f0342f5.tar.gz
smtcoq-a845071c6ab36da0cb8c82b17b461b4f2f0342f5.zip
Best practice on axiom
Diffstat (limited to 'src/BEST_PRACTICE.md')
-rw-r--r--src/BEST_PRACTICE.md3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md
index ba15070..d72c112 100644
--- a/src/BEST_PRACTICE.md
+++ b/src/BEST_PRACTICE.md
@@ -1,7 +1,8 @@
# Proofs
## Axioms
-No axiom should be added. No library adding axioms should be imported.
+No axiom should be added. No library adding axioms should be imported
+(except Int63 and Array).
# Code organization