diff options
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 *) |