aboutsummaryrefslogtreecommitdiffstats
path: root/src/BEST_PRACTICE.md
diff options
context:
space:
mode:
Diffstat (limited to 'src/BEST_PRACTICE.md')
-rw-r--r--src/BEST_PRACTICE.md8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md
index bbfd381..f75c7aa 100644
--- a/src/BEST_PRACTICE.md
+++ b/src/BEST_PRACTICE.md
@@ -9,6 +9,14 @@ except:
implemented as dependent types).
+## Hints
+
+Every hint should be put in a hint database, whose name starts with
+"smtcoq_". There should be a different database for each part of SMTCoq
+(e.g., one for each theory). The general database that is used across
+the project is named `smtcoq_core`.
+
+
# Code organization
## Documentation
Every OCaml module comes with a documented interface.