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.
---
 plugins/syntax/numeral_notation_plugin.mlpack | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 plugins/syntax/numeral_notation_plugin.mlpack

(limited to 'plugins/syntax/numeral_notation_plugin.mlpack')

diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack
new file mode 100644
index 0000000000..643c148979
--- /dev/null
+++ b/plugins/syntax/numeral_notation_plugin.mlpack
@@ -0,0 +1 @@
+G_numeral
-- 
cgit v1.2.3


From 6a280b70fc66ff0231a9945cc3b3718385d3971c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 14 Aug 2018 14:04:08 -0400
Subject: Move g_numeral.ml4 to numeral.ml

As per https://github.com/coq/coq/pull/8064#pullrequestreview-145971522
---
 plugins/syntax/numeral_notation_plugin.mlpack | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/syntax/numeral_notation_plugin.mlpack')

diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack
index 643c148979..f4d9cae3ff 100644
--- a/plugins/syntax/numeral_notation_plugin.mlpack
+++ b/plugins/syntax/numeral_notation_plugin.mlpack
@@ -1 +1,2 @@
+Numeral
 G_numeral
-- 
cgit v1.2.3