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/grammar_API.ml | 63 ------------------------------------------------------
 1 file changed, 63 deletions(-)
 delete mode 100644 API/grammar_API.ml

(limited to 'API/grammar_API.ml')

diff --git a/API/grammar_API.ml b/API/grammar_API.ml
deleted file mode 100644
index 485c166657..0000000000
--- a/API/grammar_API.ml
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module G_proofs = G_proofs
-module Metasyntax = Metasyntax
-module Egramcoq = Egramcoq
-module G_vernac = G_vernac
-module Pcoq = Pcoq
-module Tok = Tok
-module CLexer = CLexer
-module Egramml = Egramml
-module Mltop = Mltop
-module Vernacinterp = Vernacinterp
-module Genintern = Genintern
-
-module Extend =
-  struct
-    type 'a entry = 'a Extend.entry
-    type ('self, 'a) symbol = ('self, 'a) Extend.symbol =
-                            | Atoken : Tok.t -> ('self, string) symbol
-                            | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
-                            | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
-                            | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
-                            | Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
-                            | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
-                            | Aself : ('self, 'self) symbol
-                                      | Anext : ('self, 'self) symbol
-                                                | Aentry : 'a entry -> ('self, 'a) symbol
-                            | Aentryl : 'a entry * int -> ('self, 'a) symbol
-                            | Arules : 'a rules list -> ('self, 'a) symbol
-     and ('self, 'a, 'r) rule = ('self, 'a, 'r) Extend.rule =
-                              | Stop : ('self, 'r, 'r) rule
-                                       | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
-     and ('a, 'r) norec_rule = ('a, 'r) Extend.norec_rule =
-                                 { norec_rule : 's. ('s, 'a, 'r) rule }
-     and 'a rules = 'a Extend.rules =
-                  | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
-    type gram_assoc = Extend.gram_assoc = NonA | RightA | LeftA
-    type 'a production_rule = 'a Extend.production_rule =
-                            | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-    type 'a single_extend_statment = string option * gram_assoc option * 'a production_rule list
-    type gram_position = Extend.gram_position =
-      | First
-      | Last
-      | Before of string
-      | After of string
-      | Level of string
-    type 'a extend_statment = Extend.gram_position option * 'a single_extend_statment list
-
-    type 'a user_symbol = 'a Extend.user_symbol =
-                        | Ulist1 of 'a user_symbol
-                        | Ulist1sep of 'a user_symbol * string
-                        | Ulist0 of 'a user_symbol
-                        | Ulist0sep of 'a user_symbol * string
-                        | Uopt of 'a user_symbol
-                        | Uentry of 'a
-                        | Uentryl of 'a * int
-  end
-- 
cgit v1.2.3