X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommPcsAnd.ml;h=cf09e52ce1dd850817c238608a6bd0989f9eccba;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=de05255a557f8690b491f2f4452539b216449f89;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
index de05255a5..cf09e52ce 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
@@ -1,22 +1,20 @@
 module EC = RecommCheck
 module ES = RecommStep
+module ET = RecommTypes
 
 module D = RecommGcsWith
 
 let b_line = ref ES.id
 
-let rec k_and k ok outs ins =
-  if ok then begin
-    match ins with
-    | "and" :: tl -> step k false ("and" :: outs) tl
-    | _           -> k true outs ins
-  end else begin
-    k true outs ins
-  end
+let rec k_and k st outs ins =
+  if st <> ET.OK then k ET.KO outs ins else
+  match ins with
+  | "and" :: tl -> step k ET.OK ("and" :: outs) tl
+  | _           -> k ET.OK outs ins
 
-and step k ok outs ins =
-  if ok then k ok outs ins else
-  !b_line (k_and k) ok outs ins
+and step k st outs ins =
+  if st <> ET.OK then k st outs ins else
+  !b_line (k_and k) ET.OO outs ins 
 
 let register_b =
   ES.register b_line