]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/lib/share.ml
- new semantic log system
[helm.git] / helm / software / lambda-delta / lib / share.ml
index 019cca982ddab5b8b68335089d898ddaedffbc7e..c8097d568eac398c663e5ac5a11d7be212bd4cda 100644 (file)
@@ -11,6 +11,9 @@
 
 let sh a b =
    if a == b then a else b
-   
-let sh2 a1 b1 a2 b2 c1 c2 =
+
+let sh1 a1 a2 b1 b2 =
+   if a1 == a2 then b1 else b2 (sh a1 a2)
+
+let sh2 a1 a2 b1 b2 c1 c2 =
    if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2)