Skip to content

Commit

Permalink
[api] Remove type equalities from API.
Browse files Browse the repository at this point in the history
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`
  • Loading branch information
ejgallego committed Jul 25, 2017
1 parent b6f3c8e commit fc218c2
Show file tree
Hide file tree
Showing 37 changed files with 1,331 additions and 927 deletions.
27 changes: 21 additions & 6 deletions API/API.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
(******************************************************************************)
Expand Down Expand Up @@ -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 *)
Expand All @@ -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
Expand All @@ -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

0 comments on commit fc218c2

Please sign in to comment.