[general] Merge parsing with highparsing, put toplevel at the top of the linking chain.

10 files changed, 58 insertions, 90 deletions

diff --git a/API/API.ml b/API/API.ml
index c4bcef6f6..68da858ba 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
diff --git a/API/API.mli b/API/API.mli
index 3b2dc5a67..a80de7b2c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -10,7 +10,7 @@
    in Coq. 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
    ```
 
    Note however that files in intf/ are located manually now as their
@@ -4828,6 +4828,23 @@ sig
 
 end
 
+module G_vernac :
+sig
+
+  val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry
+  val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry
+  val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry
+
+end
+
+module G_proofs :
+sig
+
+  val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
+  val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option
+
+end
+
 (************************************************************************)
 (* End of modules from parsing/                                         *)
 (************************************************************************)
@@ -5717,28 +5734,3 @@ end
 (************************************************************************)
 (* End of modules from stm/                                             *)
 (************************************************************************)
-
-(************************************************************************)
-(* Modules from highparsing/                                            *)
-(************************************************************************)
-
-module G_vernac :
-sig
-
-  val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry
-  val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry
-  val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry
-
-end
-
-module G_proofs :
-sig
-
-  val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
-  val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option
-
-end
-
-(************************************************************************)
-(* End of modules from highparsing/                                     *)
-(************************************************************************)
diff --git a/META.coq b/META.coq
index e70b8e28d..27aeac61b 100644
--- a/META.coq
+++ b/META.coq
@@ -228,6 +228,32 @@ package "stm" (
 
 )
 
+package "API" (
+
+  description = "Coq API"
+  version     = "8.7"
+
+  requires    = "coq.stm"
+  directory   = "API"
+
+  archive(byte)    = "API.cma"
+  archive(native)  = "API.cmxa"
+
+)
+
+package "ltac" (
+
+  description = "Coq LTAC Plugin"
+  version     = "8.7"
+
+  requires    = "coq.API"
+  directory   = "plugins/ltac"
+
+  archive(byte)    = "ltac_plugin.cmo"
+  archive(native)  = "ltac_plugin.cmx"
+
+)
+
 package "toplevel" (
 
   description = "Coq Toplevel"
@@ -254,6 +280,7 @@ package "idetop" (
 
 )
 
+# XXX Depends on way less than toplevel
 package "ide" (
 
   description = "Coq IDE Libraries"
@@ -267,44 +294,3 @@ package "ide" (
   archive(native)  = "ide.cmxa"
 
 )
-
-# XXX: Remove the dependency on toplevel (due to Coqinit use for compat flags)
-package "highparsing" (
-
-  description = "Coq Extra Parsing"
-  version     = "8.7"
-
-  requires    = "coq.toplevel"
-  directory   = "parsing"
-
-  archive(byte)    = "highparsing.cma"
-  archive(native)  = "highparsing.cmxa"
-
-)
-
-# XXX: API should depend only on stm.
-package "API" (
-
-  description = "Coq API"
-  version     = "8.7"
-
-  requires    = "coq.highparsing"
-  directory   = "API"
-
-  archive(byte)    = "API.cma"
-  archive(native)  = "API.cmxa"
-
-)
-
-package "ltac" (
-
-  description = "Coq LTAC Plugin"
-  version     = "8.7"
-
-  requires    = "coq.API"
-  directory   = "plugins/ltac"
-
-  archive(byte)    = "ltac_plugin.cmo"
-  archive(native)  = "ltac_plugin.cmx"
-
-)
diff --git a/Makefile.common b/Makefile.common
index ccbe9261e..4d63b08e2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -105,7 +105,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
-	parsing/highparsing.cma stm/stm.cma toplevel/toplevel.cma API/API.cma
+	stm/stm.cma toplevel/toplevel.cma API/API.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
diff --git a/Makefile.dev b/Makefile.dev
index b0299bd16..dc4ded397 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -116,12 +116,11 @@ tactics: tactics/tactics.cma
 interp: interp/interp.cma
 parsing: parsing/parsing.cma
 pretyping: pretyping/pretyping.cma
-highparsing: parsing/highparsing.cma
 stm: stm/stm.cma
 toplevel: toplevel/toplevel.cma
 
 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API
-.PHONY: engine highparsing stm toplevel
+.PHONY: engine stm toplevel
 
 ######################
 ### 3) theories files
diff --git a/Makefile.doc b/Makefile.doc
index dd7717359..3f8ae3680 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -470,7 +470,7 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
 ml-doc:
 	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
 
-parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
+parsing/parsing.dot : | parsing/parsing.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
 grammar/grammar.dot : | grammar/grammar.mllib.d
diff --git a/dev/core.dbg b/dev/core.dbg
index 71d06cdb0..18e82c352 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,7 +16,6 @@ load_printer tactics.cma
 load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
-load_printer highparsing.cma
 load_printer intf.cma
 load_printer API.cma
 load_printer ltac_plugin.cmo
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 00e7f5c53..2dbd132da 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -14,11 +14,6 @@ parsing
 tactics
 toplevel
 
-highparsing :
-
- Files in parsing/ that cannot be linked too early.
- Contains the grammar rules g_*.ml4
-
 Special components
 ------------------
 
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
deleted file mode 100644
index 05e2911c2..000000000
--- a/parsing/highparsing.mllib
+++ /dev/null
@@ -1,4 +0,0 @@
-G_constr
-G_vernac
-G_prim
-G_proofs
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2a73d7bc6..1f29636b2 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -3,3 +3,7 @@ CLexer
 Pcoq
 Egramml
 Egramcoq
+G_constr
+G_vernac
+G_prim
+G_proofs