update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml
new file mode 100644 (file)
index 0000000..52a1c00
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml
@@ -0,0 +1,17 @@
+module EC = RecommCheck
+module ES = RecommStep
+module ET = RecommTypes
+
+module D = RecommPcsAnd
+
+let p_line = ref ES.id
+
+let step k st outs ins =
+  if st = ET.KO then k st outs ins else
+  !p_line k ET.OO outs ins
+
+let register_p =
+  ES.register p_line
+
+let main =
+  EC.register_s step