aboutsummaryrefslogtreecommitdiff
path: root/API/PROPERTIES
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-12 16:20:15 +0200
committerMaxime Dénès2017-06-12 16:43:33 +0200
commit9097e9a84cf3841cd5fac81a7fe309ae2dec246f (patch)
tree7358a5db6e5f6f17974cc61b4491248f30a332b4 /API/PROPERTIES
parent013c0232953f1f5832c30940119da05847e99ce2 (diff)
parentb6feaafc7602917a8ef86fb8adc9651ff765e710 (diff)
Merge PR#718: API cleanup: aliases
Diffstat (limited to 'API/PROPERTIES')
-rw-r--r--API/PROPERTIES8
1 files changed, 8 insertions, 0 deletions
diff --git a/API/PROPERTIES b/API/PROPERTIES
new file mode 100644
index 0000000000..cd942e2021
--- /dev/null
+++ b/API/PROPERTIES
@@ -0,0 +1,8 @@
+0 : All API elements, i.e.:
+ - modules
+ - module types
+ - functions & values
+ - types
+ are present if and only if are needed for implementing Coq plugins.
+
+1 : Individual API elements are not aliased.