]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/layer.ml
- we add the missing layer constraint on applicability condition
[helm.git] / helm / software / helena / src / common / layer.ml
index d781003249fb355d458cc647d7c3ac7644db642b..494b3915937027a1ee5f96227416edb3f0cd6708 100644 (file)
@@ -30,11 +30,11 @@ type status = (J.mark, layer) H.t (* environment for layer variables *)
 
 (* Internal functions *******************************************************)
 
-let level = 6
+let level = 7
 
 let env_size = 1300
 
-let warn s = L.warn level s
+let warn s = L.warn (pred level) s
 
 let zero = Fin 0