X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommPccFor.ml;h=41a787dbd3c5dbeea522cb341b9b838723a56731;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=cdad8df5599a13ce628bc91706fc2a74fba35482;hpb=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
index cdad8df55..41a787dbd 100644
--- 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