X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommGcbGroundArith.ml;h=c2f4481139dafc4a961b093766598d0a0cc3b063;hb=2ed8d2abcc3b0687141b627061b63350a0b200bd;hp=d9f7a0d1002d6a5be3c76f2e028c9a6fa1acb135;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
index d9f7a0d10..c2f448113 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
@@ -16,12 +16,18 @@ let step k st outs ins =
   | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
   | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
   | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
+  | "nrplus" :: tl -> k T.OK ("nrplus" :: outs) tl
+  | "rplus" :: tl -> k T.OK ("nrplus" :: outs) tl
   | "npred" :: tl -> k T.OK ("npred" :: outs) tl
   | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
+  | "npsucc" :: tl -> k T.OK ("npsucc" :: outs) tl
   | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
   | "niter" :: tl -> k T.OK ("niter" :: outs) tl
   | "plt" :: tl -> k T.OK ("plt" :: outs) tl
   | "ple" :: tl -> k T.OK ("ple" :: outs) tl
+  | "pplus" :: tl -> k T.OK ("pplus" :: outs) tl
+  | "ppred" :: tl -> k T.OK ("ppred" :: outs) tl
+  | "psucc" :: tl -> k T.OK ("psucc" :: outs) tl
   | _ -> k T.OO outs ins
 
 let main =