aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-10 10:59:22 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-06-07 14:49:13 +0200
commit661940fd55a925a6f17f6025f5d15fc9f5647cf9 (patch)
treeeee305047751a333fd8aeff625c775ce8ed58013 /lib
parent73fd3afba9e8917dfc0644d1d8d9b22063cfa2fe (diff)
Put all plugins behind an "API".
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index bc8012297..2f76183eb 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -206,7 +206,7 @@ let coq_src_subdirs = [
"config" ; "dev" ; "lib" ; "kernel" ; "library" ;
"engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
"tactics" ; "toplevel" ; "printing" ; "intf" ;
- "grammar" ; "ide" ; "stm"; "vernac" ] @
+ "grammar" ; "ide" ; "stm"; "vernac" ; "API" ] @
Coq_config.plugins_dirs
let print_config ?(prefix_var_name="") f =