From 6ddb77f5f60db1006c95552f893a71dd7571d966 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 6 Jul 2020 12:39:51 +0200
Subject: Clarify axiom usage (closes #71)

---
 src/BEST_PRACTICE.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md
index 783ef82..bbfd381 100644
--- a/src/BEST_PRACTICE.md
+++ b/src/BEST_PRACTICE.md
@@ -1,8 +1,12 @@
 # Proofs
 ## Axioms
 
-No axiom should be added. No library adding axioms should be imported
-(except Int63 and Array).
+No axiom should be added. No library adding axioms should be imported,
+except:
+- Int63 and Array, used in core SMTCoq
+- ProofIrrelevance, to be used with care (it is currently used only to
+  treat equality over bit vectors and functional arrays, which are
+  implemented as dependent types).
 
 
 # Code organization
-- 
cgit