milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
index 1528eb2b1ef9ca2707ad49d8712450614e7fa7b3..d9f7a0d1002d6a5be3c76f2e028c9a6fa1acb135 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
@@ -20,6 +20,8 @@ let step k st outs ins =
   | "nsucc" :: tl -> k T.OK ("nsucc" :: 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
   | _ -> k T.OO outs ins
 
 let main =