]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/layer.ml
now type inclusion is correctly managed in the RTM
[helm.git] / helm / software / helena / src / common / layer.ml
index 61254620f192ecd21edad2a1c0a13476a8654a37..d781003249fb355d458cc647d7c3ac7644db642b 100644 (file)
@@ -34,10 +34,10 @@ let level = 6
 
 let env_size = 1300
 
-let zero = Fin 0
-
 let warn s = L.warn level s
 
+let zero = Fin 0
+
 let string_of_value k = function
    | Inf        -> ""
    | Fin i      -> string_of_int i
@@ -185,3 +185,6 @@ let assert_equal st n1 n2 =
    if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
       n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
    end; b end
+
+let is_not_zero st n  =
+   let _, n = resolve_layer st n in n.v <> zero