Parsing files for numerals (+ ascii/string) moved into plugins

 Idea: make coqtop more independant of the standard library.
 In the future, we can imagine loading the syntax for numerals right
 after their definition. For the moment, it is easier to stay lazy
 and load the syntax plugins slightly before the definitions.

 After this commit, the main (sole ?) references to theories/
 from the core ml files are in Coqlib (but many parts of coqlib
 are only used by plugins), and it mainly concerns Init
 (+ Logic/JMeq and maybe a few others).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 35 insertions, 12 deletions

diff --git a/Makefile.common b/Makefile.common
index b17d371955..5a2817e419 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -69,7 +69,7 @@ SRCDIRS:=\
     omega	romega 		micromega 	quote		ring	dp \
     setoid_ring xml 		extraction 	interface 	fourier \
     cc 		funind 		firstorder 	field 		subtac \
-    rtauto 	groebner )
+    rtauto 	groebner        syntax)
 
 # Order is relevent here because kernel and checker contain files
 # with the same name
@@ -176,17 +176,24 @@ FOCMA:=plugins/firstorder/ground_plugin.cma
 CCCMA:=plugins/cc/cc_plugin.cma
 SUBTACCMA:=plugins/subtac/subtac_plugin.cma
 RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
+NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
+OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
+        z_syntax_plugin.cma \
+        numbers_syntax_plugin.cma \
+        r_syntax_plugin.cma \
+	ascii_syntax_plugin.cma \
+        string_syntax_plugin.cma )
 
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
         $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
         $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
         $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
-        $(FUNINDCMA) $(GBCMA)
+        $(FUNINDCMA) $(GBCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
 
 ifneq ($(HASNATDYNLINK),false)
  STATICPLUGINS:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
-	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA)
+	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  PLUGINS:=$(PLUGINSCMA)
  PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 03fb9c6295..3eb27abbb6 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -4,10 +4,4 @@ G_prim
 G_proofs
 G_tactic
 G_ltac
-G_natsyntax
-G_zsyntax
-G_rsyntax
-G_ascii_syntax
-G_string_syntax
 G_decl_mode
-G_intsyntax
diff --git a/parsing/g_ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index f9ca94ff6c..f9ca94ff6c 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib
new file mode 100644
index 0000000000..54b5815c5e
--- /dev/null
+++ b/plugins/syntax/ascii_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Ascii_syntax
+Ascii_syntax_mod
diff --git a/parsing/g_natsyntax.ml b/plugins/syntax/nat_syntax.ml
index c62c813778..c62c813778 100644
--- a/parsing/g_natsyntax.ml
+++ b/plugins/syntax/nat_syntax.ml
diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib
new file mode 100644
index 0000000000..35af248197
--- /dev/null
+++ b/plugins/syntax/nat_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Nat_syntax
+Nat_syntax_mod
diff --git a/parsing/g_intsyntax.ml b/plugins/syntax/numbers_syntax.ml
index 7cef2fac00..94e4c103a9 100644
--- a/parsing/g_intsyntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -205,7 +205,7 @@ let bigN_of_pos_bigint dloc n =
   let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then
 				                       [word]
 			                             else
-				                      [G_natsyntax.nat_of_int dloc (sub h n_inlined);
+				                      [Nat_syntax.nat_of_int dloc (sub h n_inlined);
 						       word])
   in
   let hght = height n in
diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib
new file mode 100644
index 0000000000..060f47c1f0
--- /dev/null
+++ b/plugins/syntax/numbers_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Numbers_syntax
+Numbers_syntax_mod
diff --git a/parsing/g_rsyntax.ml b/plugins/syntax/r_syntax.ml
index 4a5972cc71..4a5972cc71 100644
--- a/parsing/g_rsyntax.ml
+++ b/plugins/syntax/r_syntax.ml
diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib
new file mode 100644
index 0000000000..b9ea91db3e
--- /dev/null
+++ b/plugins/syntax/r_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+R_syntax
+R_syntax_mod
diff --git a/parsing/g_string_syntax.ml b/plugins/syntax/string_syntax.ml
index a936485d9b..d1c263dc8c 100644
--- a/parsing/g_string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -14,7 +14,7 @@ open Names
 open Pcoq
 open Libnames
 open Topconstr
-open G_ascii_syntax
+open Ascii_syntax
 open Rawterm
 open Coqlib
 
diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib
new file mode 100644
index 0000000000..f73c447c82
--- /dev/null
+++ b/plugins/syntax/string_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+String_syntax
+String_syntax_mod
diff --git a/parsing/g_zsyntax.ml b/plugins/syntax/z_syntax.ml
index bfbe54c28c..bfbe54c28c 100644
--- a/parsing/g_zsyntax.ml
+++ b/plugins/syntax/z_syntax.ml
diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib
new file mode 100644
index 0000000000..cabaef8202
--- /dev/null
+++ b/plugins/syntax/z_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Z_syntax
+Z_syntax_mod
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 73e4924aaa..2194b93a3f 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -12,6 +12,8 @@ Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Logic.
+Declare ML Module "nat_syntax_plugin".
+
 
 (** [unit] is a singleton datatype with sole inhabitant [tt] *)
 
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 84de55e24d..685c724703 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,7 +15,8 @@ Require Export Specif.
 Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
-(* Initially available plugins *)
+(* Initially available plugins
+   (+ nat_syntax_plugin loaded in Datatypes) *)
 Declare ML Module "extraction_plugin".
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 209eb5497f..076bceba48 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -10,6 +10,8 @@
 
 Unset Boxed Definitions.
 
+Declare ML Module "z_syntax_plugin".
+
 (**********************************************************************)
 (** Binary positive numbers *)
 
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 633cc84230..d890d9287b 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -21,6 +21,8 @@ Require Export ZArith.
 Require Export Znumtheory.
 Require Export Zpow_facts.
 
+Declare ML Module "numbers_syntax_plugin".
+
 (* *** Nota Bene ***
    All results that were general enough has been moved in ZArith.
    Only remain here specialized lemmas and compatibility elements.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 63b8928fb2..897d5c7100 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -12,6 +12,7 @@
 (**          Definitions for the axiomatization          *)
 (*********************************************************)
 
+Declare ML Module "r_syntax_plugin".
 Require Export ZArith_base.
 
 Parameter R : Set.
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 1f10f2affd..5a2cc96957 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -13,6 +13,7 @@
 
 Require Import Bool.
 Require Import BinPos.
+Declare ML Module "ascii_syntax_plugin".
 
 (** * Definition of ascii characters *)
 
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 59edf81871..7d6696b782 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -13,6 +13,7 @@
 
 Require Import Arith.
 Require Import Ascii.
+Declare ML Module "string_syntax_plugin".
 
 (** *** Definition of strings *)