1 files changed, 0 insertions, 26 deletions
diff --git a/theories/Num/Nat/NSyntax.v b/theories/Num/Nat/NSyntax.v
deleted file mode 100644
index 9752dd2e9..000000000
--- a/theories/Num/Nat/NSyntax.v
+++ /dev/null
@@ -1,26 +0,0 @@
-
-(*s Syntax for arithmetic *)
-
-Infix 6 "<" lt.
-Infix 6 "<=" le.
-Infix 6 ">" gt.
-Infix 6 ">=" ge.
-
-(*i Infix 7 "+" plus. i*)
-
-Grammar constr lassoc_constr4 :=
-  squash_sum
-  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
-      case [$c2] of
-        (SQUASH $T2) ->
-            case [$c1] of
-              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
-            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
-            esac
-      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
-      esac.
-
-Syntax constr
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-\ No newline at end of file