]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgCrg.ml
- new attributes system
[helm.git] / helm / software / helena / src / basic_rg / brgCrg.ml
index f646145ed65c2047f66bc3d5f64845fdf2afbc3e..a392afe93b708178be8a727a0444d3092e0c9ab9 100644 (file)
@@ -11,7 +11,6 @@
 
 module C = Cps
 module E = Entity
-module J = Marks
 module N = Level
 module D = Crg
 module B = Brg
@@ -37,7 +36,7 @@ let rec xlate_term f = function
 
 and xlate_bind f a b x = match b with
    | D.Abst (n, w) ->
-      let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in 
+      let f ww = f (B.Bind (a, B.Abst (n, ww), x)) in 
       xlate_term f w
    | D.Abbr v      ->
       let f vv = f (B.Bind (a, B.Abbr vv, x)) in