X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2FmetaAut.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2FmetaAut.ml;h=be63450076cbaa964424735f74c9eeb856bb07f3;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=6a45518b5bbf1210f5f46d6ffa620a66e000fc3e;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.ml b/helm/software/lambda-delta/src/toplevel/metaAut.ml
index 6a45518b5..be6345007 100644
--- a/helm/software/lambda-delta/src/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/src/toplevel/metaAut.ml
@@ -14,6 +14,7 @@ module K = U.UriHash
 module C = Cps
 module G = Options
 module E = Entity
+module N = Level
 module M = Meta
 module A = Aut
 
@@ -179,7 +180,7 @@ let xlate_entity err f st = function
 	       K.add henv (uri_of_qid qid) pars;
 	       let a = [E.Mark st.line] in
 	       let entry = pars, ww, None in
-	       let entity = a, uri_of_qid qid, E.Abst entry in
+	       let entity = a, uri_of_qid qid, E.Abst (N.infinite, entry) in
 	       f {st with line = succ st.line} entity
 	    in
 	    xlate_term f st pars w