update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
index cdad8df5599a13ce628bc91706fc2a74fba35482..41a787dbd3c5dbeea522cb341b9b838723a56731 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
@@ -1,26 +1,28 @@
 module EC = RecommCheck
 module ES = RecommStep
+module ET = RecommTypes
 
 let d_line = ref ES.id
 
 let r_line = ref ES.id
 
-let k_for k ok outs ins =
-  if ok then begin
-    match ins with
-    | "FOR" :: tl -> !d_line k false ("FOR" :: outs) tl
-    | _           -> k true outs ins
-  end else begin
-    k true outs ins
-  end
-
-let k_or k ok outs ins =
-  if ok then k ok outs ins else
-  !r_line (k_for k) ok outs ins
-
-let step k ok outs ins =
-  if ok then k ok outs ins else
-  !d_line (k_or k) ok outs ins
+let k_exit k st out ins =
+  if st <> ET.OK then k ET.KO out ins else
+  k st out ins
+
+let k_for k st outs ins =
+  if st <> ET.OK then k ET.KO outs ins else
+  match ins with
+  | "FOR" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
+  | _           -> k ET.KO outs ins
+
+let k_or k st outs ins =
+  if st <> ET.OO then k st outs ins else
+  !r_line (k_for k) st outs ins
+
+let step k st outs ins =
+  if st = ET.KO then k st outs ins else
+  !d_line (k_or k) ET.OO outs ins
 
 let register_d =
   ES.register d_line