propagating the arithmetics library, partial commit

[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 5d08261c860b3de123ccde2f9bcc5f73dc58e2d0..cdad8df5599a13ce628bc91706fc2a74fba35482 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
@@ -8,7 +8,7 @@ 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
+    | "FOR" :: tl -> !d_line k false ("FOR" :: outs) tl
     | _           -> k true outs ins
   end else begin
     k true outs ins