diff options
| author | Emilio Jesus Gallego Arias | 2017-07-20 17:10:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-07-25 16:07:32 +0200 |
| commit | fc218c26cfb226be25c344af50b4b86e52360934 (patch) | |
| tree | fd0650fa1fc981c81e62991d8d8e97431312285e /API/API.ml | |
| parent | b6f3c8e4f173e3f272f966e1061e7112bf5d1b4a (diff) | |
[api] Remove type equalities from API.
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
Diffstat (limited to 'API/API.ml')
| -rw-r--r-- | API/API.ml | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/API/API.ml b/API/API.ml index fd20167f21..c952e123d4 100644 --- a/API/API.ml +++ b/API/API.ml @@ -39,15 +39,15 @@ module Context = Context module Vars = Vars module Term = Term module Mod_subst = Mod_subst -(* module Cbytecodes *) +module Cbytecodes = Cbytecodes (* module Copcodes *) -(* module Cemitcodes *) +module Cemitcodes = Cemitcodes (* module Nativevalues *) (* module Primitives *) module Opaqueproof = Opaqueproof module Declareops = Declareops module Retroknowledge = Retroknowledge -(* module Conv_oracle *) +module Conv_oracle = Conv_oracle (* module Pre_env *) (* module Cbytegen *) (* module Nativelambda *) @@ -166,7 +166,7 @@ module Unification = Unification (* interp *) (******************************************************************************) module Stdarg = Stdarg -(* module Genintern *) +module Genintern = Genintern module Constrexpr_ops = Constrexpr_ops module Notation_ops = Notation_ops module Ppextend = Ppextend @@ -216,6 +216,15 @@ module Printer = Printer module Ppvernac = Ppvernac (******************************************************************************) +(* Parsing *) +(******************************************************************************) +module Tok = Tok +module CLexer = CLexer +module Pcoq = Pcoq +module Egramml = Egramml +(* Egramcoq *) + +(******************************************************************************) (* Tactics *) (******************************************************************************) (* module Dnet *) @@ -249,7 +258,7 @@ module Himsg = Himsg module ExplainErr = ExplainErr (* module Class *) module Locality = Locality -(* module Metasyntax *) +module Metasyntax = Metasyntax (* module Auto_ind_decl *) module Search = Search (* module Indschemes *) @@ -258,7 +267,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) -(* module Vernacinterp *) +module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt module Vernacentries = Vernacentries @@ -268,3 +277,9 @@ module Vernacentries = Vernacentries (******************************************************************************) module Vernac_classifier = Vernac_classifier module Stm = Stm + +(******************************************************************************) +(* Highparsing *) +(******************************************************************************) +module G_vernac = G_vernac +module G_proofs = G_proofs |