matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml

   1 module EC = RecommCheck
   2 module ES = RecommStep
   3
   4 module D = RecommGcsWith
   5
   6 let b_line = ref ES.id
   7
   8 let rec k_and k ok outs ins =
   9   if ok then begin
  10     match ins with
  11     | "and" :: tl -> step k false ("and" :: outs) tl
  12     | _           -> k true outs ins
  13   end else begin
  14     k true outs ins
  15   end
  16
  17 and step k ok outs ins =
  18   if ok then k ok outs ins else
  19   !b_line (k_and k) ok outs ins
  20
  21 let register_b =
  22   ES.register b_line
  23
  24 let main =
  25   EC.register_s step