update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
index de05255a557f8690b491f2f4452539b216449f89..cf09e52ce1dd850817c238608a6bd0989f9eccba 100644 (file)
--- 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