- bugfix is refreshed state of AutCrg: now we return a fresh state

[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 1c2759d15d7cdfa06f1ef55239e8d11013ebd6ab..a92b6fea98f44b696c10675650a5317bcafcdf40 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -13,9 +13,8 @@ module U  = NUri
 module UH = U.UriHash
 module C  = Cps
 module G  = Options
-module N  = Level
+module N  = Layer
 module E  = Entity
-module S  = Status
 module A  = Aut
 module D  = Crg
 
@@ -127,12 +126,13 @@ let rec xlate_term f st lst y lenv = function
       let name = Some (name, true) in
       let f aw ww = 
          let f at tt =
-            let l = if !G.cc then match y, at.E.n_degr with
-               | true, _ -> N.one
-               | _   , 0 -> N.one
-               | _   , 1 -> N.unknown st.S.lenv
-               | _   , 2 -> N.two
-               | _       -> assert false
+            let l = 
+               if !G.cc then match y, at.E.n_degr with
+                  | true, _ -> N.one
+                  | _   , 0 -> N.one
+                  | _   , 1 -> N.unknown st
+                  | _   , 2 -> N.two
+                  | _       -> assert false
                else N.infinite
             in
            let b = D.Abst (l, ww) in
@@ -207,7 +207,7 @@ let xlate_entity err f st lst = function
         in
          complete_qid f lst (name, true, [])
       in
-      get_cnt_relaxed (D.sta f) lst
+      get_cnt_relaxed (D.replace f N.one) lst
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid = 
@@ -239,8 +239,6 @@ let initial_status () =
    path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ();
 }
 
-let refresh_status lst = {lst with
-   mk_uri = G.get_mk_uri ()
-}
+let refresh_status lst = initial_status ()
 
 let crg_of_aut = xlate_entity