From 7f2c52bcf588abfcbf30530bae240244229304a4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 27 Mar 2009 17:53:43 +0000
Subject: 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
---
 Makefile.common | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'Makefile.common')

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)
-- 
cgit v1.2.3