From 6eefbf216bd4d674f84a7827ecb205c6e12c33d3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 26 Aug 2016 15:15:44 +0200
Subject: A proposal for recommended uniformity of style in programming Coq.

Starting listing some recommendations in using the API.
---
 dev/doc/api.txt | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 dev/doc/api.txt

(limited to 'dev/doc/api.txt')

diff --git a/dev/doc/api.txt b/dev/doc/api.txt
new file mode 100644
index 0000000000..5827257b53
--- /dev/null
+++ b/dev/doc/api.txt
@@ -0,0 +1,10 @@
+Recommendations in using the API:
+
+The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
+
+- On type constr, the canonical equality on CIC (up to
+  alpha-conversion and cast removal) is Constr.equal
+- The type constr is abstract, use mkRel, mkSort, etc. to build
+  elements in constr; use "kind_of_term" to analyze the head of a
+  constr; use destRel, destSort, etc. when the head constructor is
+  known
-- 
cgit v1.2.3