From b786723fe7aff0c58ac949d44a356e2df6805645 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 22 Feb 2017 23:15:24 +0100
Subject: Numeral Notation (for inductive types)

 This is a portion of roglo's PR#156 introducing a Numeral Notation
 command : we deal here with inductive types via conversion fonctions
 from/to Z written in Coq.

 For an example, see plugins/syntax/NatSyntaxViaZ.v

 This commit does not include the part about printing via some ltac.
 Using ltac was meant for dealing with real numbers, let's see first what
 become PR#415 about a compact representation for real literals.
---
 Makefile.common | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 772561bd70..4f09fb376a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -146,7 +146,8 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         z_syntax_plugin.cmo r_syntax_plugin.cmo \
 	int31_syntax_plugin.cmo \
 	ascii_syntax_plugin.cmo \
-        string_syntax_plugin.cmo )
+        string_syntax_plugin.cmo \
+	numeral_notation_plugin.cmo)
 DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
-- 
cgit v1.2.3


From ec0ad20de8daf2ad9f3237de92a745247db845f5 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 21 Mar 2017 16:13:24 +0100
Subject: remove legacy syntax plugins subsumed by Numeral Notation

---
 Makefile.common | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 4f09fb376a..09457ced7b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -140,10 +140,8 @@ FOCMO:=plugins/firstorder/ground_plugin.cmo
 CCCMO:=plugins/cc/cc_plugin.cmo
 BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo
 RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
-NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
-OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
-        positive_syntax_plugin.cmo n_syntax_plugin.cmo \
-        z_syntax_plugin.cmo r_syntax_plugin.cmo \
+SYNTAXCMO:=$(addprefix plugins/syntax/, \
+        r_syntax_plugin.cmo \
 	int31_syntax_plugin.cmo \
 	ascii_syntax_plugin.cmo \
         string_syntax_plugin.cmo \
@@ -157,7 +155,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
         $(QUOTECMO) $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
-        $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
+        $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
 	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
-- 
cgit v1.2.3