update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
index 7005e5c2046f60637e2bd7a425623754a17b268b..dfefb2f549c2fd2f41b3e534f521d8a99154b63f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
@@ -4,6 +4,7 @@ module R = RecommPcsPar
 let step k st outs ins =
   if st <> T.OO then k st outs ins else
   match ins with
+  | "(decidability)" :: tl -> k T.OK ("(decidability)" :: outs) tl
   | "(semigroup" :: "properties)" :: tl -> k T.OK ("properties)" :: "(semigroup" :: outs) tl
   | _ -> k T.OO outs ins