diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-12-22 14:11:55 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-12-27 14:19:59 +0100 |
| commit | b37d3f199e4521e2ae20cc96f0f2b04acc36c7cc (patch) | |
| tree | 5286af838087a280405b1cf1c7a3248612e7c5aa /dev/base_include | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
[API] remove large file containing duplicate interfaces
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include index 4dc9a0bee..2a4ad4a15 100644 --- a/dev/base_include +++ b/dev/base_include @@ -18,12 +18,10 @@ #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";; @@ -194,7 +192,7 @@ let qid = Libnames.qualid_of_string;; let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;; -let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of implicit syntax *) |