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

1 files changed, 19 insertions, 27 deletions

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/                                     *)
-(************************************************************************)