]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/complete_rg/crgTxt.ml
the old intermediate language (meta) is now obsolete
[helm.git] / helm / software / lambda-delta / src / complete_rg / crgTxt.ml
index 141b467bbeb2d6a8a6bcd574e61ffaa2b3ff4c51..980b74a08302db7565957933d512ab65c0664666 100644 (file)
@@ -73,16 +73,16 @@ let rec xlate_term f st lenv = function
       let abst_map (lenv, a, wws) (id, r, w) = 
          let attr = name_of_id ~r id in
         let ww = xlate_term C.start st lenv w in
-        D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+        D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
       in
       let abbr_map (lenv, a, wws) (id, w) = 
          let attr = name_of_id id in
         let ww = xlate_term C.start st lenv w in
-        D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+        D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
       in
       let void_map (lenv, a, n) id = 
         let attr = name_of_id id in
-        D.push2 C.err C.start lenv attr (), attr :: a, succ n
+        D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
       in
       let lenv, aa, bb = match b with
          | T.Abst xws ->