- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 69a8c072d2282921b958e0a96f516c1d93c761a9..0a7a46de47a21f762db9bf6b56181c8ee535437a 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -12,7 +12,6 @@
 module U = NUri
 module K = U.UriHash
 module C = Cps
-module J = Marks
 module N = Level
 module E = Entity
 module G = Options
@@ -124,7 +123,7 @@ let rec xlate_term f st lst y lenv = function
             let l = if !G.cc then match y, d with
                | true, _ -> N.one
                | _   , 0 -> N.one
-               | _   , 1 -> N.unknown st.S.lenv (J.new_mark ())
+               | _   , 1 -> N.unknown st.S.lenv
                | _   , 2 -> N.two
                | _       -> assert false
                else N.infinite
@@ -200,7 +199,7 @@ let xlate_entity err f st lst = function
         in
          complete_qid f lst (name, true, [])
       in
-      get_cnt_relaxed f lst
+      get_cnt_relaxed (D.sta f) lst
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid =