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