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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
index 7005e5c20..dfefb2f54 100644
--- 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