update in ground

[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / recommGcrGroundArith.ml

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
index 091cc7f5f52e8fa2433cba677e18840549a66972..03f6c1ed0e34c704894f45df7e29682628106db1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
@@ -8,10 +8,10 @@ let step k st outs ins =
   | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
   | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
   | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
-  | "MAXIMUN" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
   | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
   | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
   | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
+  | "RIGHT" :: "ADDITION" :: tl -> k T.OK ("ADDITION" :: "RIGHT" :: outs) tl
   | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
   | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
   | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl