- we are moving from old (patched) management of sort inclusion

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 1c2759d15d7cdfa06f1ef55239e8d11013ebd6ab..c38e8532c203fd28b7f34ee353e906bdde8b582e 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -13,9 +13,8 @@ module U  = NUri
 module UH = U.UriHash
 module C  = Cps
 module G  = Options
-module N  = Level
+module N  = Layer
 module E  = Entity
-module S  = Status
 module A  = Aut
 module D  = Crg
 
@@ -130,7 +129,7 @@ let rec xlate_term f st lst y lenv = function
             let l = if !G.cc then match y, at.E.n_degr with
                | true, _ -> N.one
                | _   , 0 -> N.one
-               | _   , 1 -> N.unknown st.S.lenv
+               | _   , 1 -> N.unknown st
                | _   , 2 -> N.two
                | _       -> assert false
                else N.infinite