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

14 files changed, 68 insertions, 100 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 82cf20a76..901ed3528 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/                                     *)
-(************************************************************************)
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/intf/vernacexpr.ml b/intf/vernacexpr.ml
index a02f1a9d4..94e166f92 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -325,7 +325,7 @@ type vernac_expr =
 
   (* Syntax *)
   | 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
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5b044d2f0..de98415cd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1134,14 +1134,13 @@ GEXTEND Gram
 
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
-	   Metasyntax.check_infix_modifiers l;
 	   let (loc,s) = s in
-	   VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l))
+	   VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l))
 
      | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
 	 s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,(s,l))
+	 -> VernacSyntaxExtension (false, local,(s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order
         to factorize with other "Print"-based vernac entries *)
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
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index fa2b166da..5e57f5de0 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -656,7 +656,7 @@ open Decl_kinds
                      | None -> mt()
                      | Some sc -> str" :" ++ spc() ++ str sc))
         )
-      | VernacSyntaxExtension (_,(s,l)) ->
+      | VernacSyntaxExtension (_, _,(s,l)) ->
         return (
           keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
             pr_syntax_modifiers l
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 22306ac5b..4fd08b42d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -409,9 +409,10 @@ let dump_global r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax_extension locality local =
+let vernac_syntax_extension locality local infix l =
   let local = enforce_module_locality locality local in
-  Metasyntax.add_syntax_extension local
+  if infix then Metasyntax.check_infix_modifiers (snd l);
+  Metasyntax.add_syntax_extension local l
 
 let vernac_delimiters sc = function
   | Some lr -> Metasyntax.add_delimiters sc lr
@@ -1950,8 +1951,8 @@ let interp ?proof ?loc locality poly c =
   | VernacLocal _ -> assert false
 
   (* Syntax *)
-  | VernacSyntaxExtension (local,sl) ->
-      vernac_syntax_extension locality local sl
+  | VernacSyntaxExtension (infix, local,sl) ->
+      vernac_syntax_extension locality local infix sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s