]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/text/txtCrg.ml
new syntax of abstractions propagated to complete_rg
[helm.git] / helm / software / helena / src / text / txtCrg.ml
index 8a4b70b7960a5ee7aa8aa251230eeebfbdd0044e..974145812ceba879cfa95be60dacedb198ffc11b 100644 (file)
@@ -104,7 +104,7 @@ and xlate_bind st f (lenv, e) b =
       | T.Abst (n, id, r, w) ->
          let f a ww =
             let a = {a with E.n_name = name_of_id ~r id} in
-            f a (D.Abst (n, ww))
+            f a (D.Abst (false, n, ww))
          in
          xlate_term f st lenv w
       | T.Abbr (id, v)       ->