X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommGcrGroundArith.ml;h=03f6c1ed0e34c704894f45df7e29682628106db1;hp=136681a291b63f3907b44ea1bac92e538332a2c9;hb=2ed8d2abcc3b0687141b627061b63350a0b200bd;hpb=b367de0252e88d6b0476648d5ceac7e4aeffca27

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
index 136681a29..03f6c1ed0 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
@@ -11,6 +11,7 @@ let step k st outs ins =
   | "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