propagating the arithmetics library, partial commit

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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
index f2f8e87a9bfcb4fe6012932313d6a5c438de2ec1..7098edb5ca2a3994a5ada39c445e6eba0d97fed9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
@@ -18,7 +18,7 @@ type src =
 (* section *)
   | Slice of words
 (* other comment *)
-  | Other of text * text * text
+  | Other of int * text * text * text
 
 type srcs = src list
 
@@ -26,4 +26,8 @@ type ('s, 't) aproc = 's -> words -> words -> 't
 
 type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc
 
-type step = (bool, bool * words * words) astep
+type return = KO
+            | OK
+            | OO
+
+type step = (return, return * words * words) astep