diff options
| author | Matej Kosik | 2016-10-10 10:59:22 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-06-07 14:49:13 +0200 |
| commit | 661940fd55a925a6f17f6025f5d15fc9f5647cf9 (patch) | |
| tree | eee305047751a333fd8aeff625c775ce8ed58013 /dev | |
| parent | 73fd3afba9e8917dfc0644d1d8d9b22063cfa2fe (diff) | |
Put all plugins behind an "API".
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 4 | ||||
| -rw-r--r-- | dev/tools/Makefile.devel | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 1 |
4 files changed, 8 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 608624d06e..defea713d8 100644 --- a/dev/base_include +++ b/dev/base_include @@ -18,10 +18,12 @@ #directory "intf";; #directory "stm";; #directory "vernac";; +#directory "../API";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) +#load "API.cma";; #use "top_printers.ml";; #use "vm_printers.ml";; @@ -56,6 +58,8 @@ (* Open main files *) +open API +open Grammar_API open Names open Term open Vars diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel index 8dcc70cf7f..ffdb1bdca9 100644 --- a/dev/tools/Makefile.devel +++ b/dev/tools/Makefile.devel @@ -5,7 +5,7 @@ TOPDIR=. BASEDIR= -SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel +SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API default: usage noargument diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 07a47c8b7a..a1b3c81b9a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,6 +8,7 @@ (* Printers for the ocaml toplevel. *) +open API open Util open Pp open Names @@ -492,6 +493,7 @@ VERNAC COMMAND EXTEND PrintConstr END *) +open Grammar_API open Genarg open Stdarg open Egramml diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index afa94a63e0..be6b914b6b 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,3 +1,4 @@ +open API open Format open Term open Names |