- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / toplevel / metaAut.ml

diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.ml b/helm/software/lambda-delta/src/toplevel/metaAut.ml
index 6a45518b5bbf1210f5f46d6ffa620a66e000fc3e..be63450076cbaa964424735f74c9eeb856bb07f3 100644 (file)
--- 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