mise sous CVS du repertoire theories/Arith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 30 insertions, 0 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
new file mode 100755
index 000000000..ab3a00ce7
--- /dev/null
+++ b/theories/Arith/Arith.v
@@ -0,0 +1,30 @@
+
+(* $Id$ *)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Minus.
+
+Axiom My_special_variable : nat -> nat.
+Declare ML Module "g_natsyntax".
+
+Grammar nat number :=.
+
+Grammar command command10 :=
+  natural_nat [ nat:number($c) ] -> [$c].
+
+Grammar command atomic_pattern :=
+  natural_pat [ nat:number($c) ] -> [$c].
+
+Syntax constr
+  level  0:
+ myspecialvariable [<<My_special_variable>>] -> ["S"];
+  level 10:
+  S [<<(S $p)>>] -> [$p:"nat_printer"]
+| O [<<O>>] -> [ "0" ]
+.