aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2020-01-28 14:59:58 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2020-01-28 14:59:58 +0100
commitea73755e6e1b7efea8db79b9fc0cf456ed5c640f (patch)
treebcfad04058e5ecf076fa1a9b4433dc2d390caaab
parentf227beb117105cf4372187112614ce4aec1c5d9b (diff)
parenta845071c6ab36da0cb8c82b17b461b4f2f0342f5 (diff)
downloadsmtcoq-ea73755e6e1b7efea8db79b9fc0cf456ed5c640f.tar.gz
smtcoq-ea73755e6e1b7efea8db79b9fc0cf456ed5c640f.zip
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
-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 0854551..b8d9d99 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).
## Hints