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

[helm.git] / helm / software / helena / src / basic_ag / bagReduction.ml

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index 6524dda862961b0cabb5d504741237da9bb75787..287978f5064dcf1a71856d4ab0d52c6798fa546d 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -12,8 +12,8 @@
 module U  = NUri
 module C  = Cps
 module L  = Log
+module P  = Marks
 module G  = Options
-module J  = Marks
 module E  = Entity
 module Z  = Bag
 module ZO = BagOutput
@@ -28,9 +28,9 @@ type machine = {
 
 type whd_result =
    | Sort_ of int
-   | LRef_ of J.mark * Z.term option
+   | LRef_ of P.mark * Z.term option
    | GRef_ of Z.entity
-   | Bind_ of Z.attrs * J.mark * Z.term * Z.term
+   | Bind_ of Z.attrs * P.mark * Z.term * Z.term
 
 type ho_whd_result =
    | Sort of int
@@ -98,12 +98,12 @@ let rec whd f c m x =
       begin match m.s with
          | []      -> f m (Bind_ (a, l, w, t))
         | v :: tl -> 
-            let nl = J.new_mark () in
+            let nl = P.new_mark () in
            let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
            Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
       end
    | Z.Bind (a, l, b, t)         -> 
-      let nl = J.new_mark () in
+      let nl = P.new_mark () in
       let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
       Z.push "!" f m.c a nl b
 
@@ -156,7 +156,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
       | GRef_ (_, _, _, E.Abbr v1), _                      ->
         whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2)     ->
-          let l = J.new_mark () in
+          let l = P.new_mark () in
           let h c =
              let m1, m2 = inc m1, inc m2 in
              let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in