From fc218c26cfb226be25c344af50b4b86e52360934 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 20 Jul 2017 17:10:58 +0200
Subject: [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`
---
 API/API.ml | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

(limited to 'API/API.ml')

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
@@ -215,6 +215,15 @@ module Printer = Printer
 (* module Prettyp *)
 module Ppvernac = Ppvernac
 
+(******************************************************************************)
+(* Parsing                                                                    *)
+(******************************************************************************)
+module Tok = Tok
+module CLexer = CLexer
+module Pcoq = Pcoq
+module Egramml = Egramml
+(* Egramcoq *)
+
 (******************************************************************************)
 (* Tactics                                                                    *)
 (******************************************************************************)
@@ -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
-- 
cgit v1.2.3