From 028de158153de94adfcb9d1e995259d833968951 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 31 Jul 2017 14:24:11 +0200
Subject: [general] Merge parsing with highparsing, put toplevel at the top of
 the linking chain.

---
 API/API.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index c4bcef6f6c..68da858ba0 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -10,9 +10,9 @@
 
    To see such order issue the comand:
 
-```
-bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done && echo -e "\n## highparsing files" && cat parsing/highparsing.mllib' > API/link
-```
+   ```
+   bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link
+   ```
  *)
 
 (******************************************************************************)
@@ -223,6 +223,9 @@ module Pcoq = Pcoq
 module Egramml = Egramml
 (* Egramcoq *)
 
+module G_vernac = G_vernac
+module G_proofs = G_proofs
+
 (******************************************************************************)
 (* Tactics                                                                    *)
 (******************************************************************************)
@@ -276,9 +279,3 @@ 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