From cc58638a8d33084c5c9f85ab4d536307da2d7929 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 31 Jul 2017 14:22:48 +0200
Subject: [vernac] Store Infix Modifier in Vernac Notation.

This removes a dependency from `G_vernac` to `Metasyntax`.
---
 API/API.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index d1774afe54..3b2dc5a679 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3799,7 +3799,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
-- 
cgit v1.2.3


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.mli | 44 ++++++++++++++++++--------------------------
 1 file changed, 18 insertions(+), 26 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 3b2dc5a679..a80de7b2c9 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/                                     *)
-(************************************************************************)
-- 
cgit v1.2.3