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

2 files changed, 25 insertions, 36 deletions

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
diff --git a/API/API.mli b/API/API.mli
index 82cf20a764..901ed3528b 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
@@ -3820,7 +3820,7 @@ sig
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
   | VernacSyntaxExtension of
-      obsolete_locality * (lstring * syntax_modifier list)
+      bool * obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
   | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * class_rawexpr list
@@ -4853,6 +4853,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/                                         *)
 (************************************************************************)
@@ -5742,28 +5759,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/                                     *)
-(************************************************************************)