]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/layer.ml
last commit for helena 0.8.2
[helm.git] / helm / software / helena / src / common / layer.ml
index ea02538d2cd13e11d8c07798ef97ad15b773e2b6..ede703d6d787a958ab576c5b89d44470f301d7c4 100644 (file)
@@ -11,9 +11,9 @@
 
 module KH = Hashtbl
 
-module L = Log
-module P = Marks
-module G = Options
+module L  = Log
+module P  = Marks
+module G  = Options
 
 type value = Inf                 (* infinite layer *)
            | Fin of int          (* finite layer *)
@@ -192,5 +192,11 @@ let assert_equal st n1 n2 =
    end; b end
 
 let is_not_zero st n  =
-   let _, n = resolve_layer st n in n.v <> zero
+(*   let _, n = resolve_layer st n in *) n.v <> zero
 
+let are_equal st n1 n2 =
+(*
+   let _, n1 = resolve_layer st n1 in
+   let _, n2 = resolve_layer st n2 in
+*)
+   n1.v = n2.v