- helena: the improved attribute system allows to export the sorts of Pi's

[helm.git] / helm / software / helena / src / basic_rg / brgReduction.ml

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index f5ad36154a3c0227d5b647b490aa296b3d7501ff..1fd77cd5140b3cdaf7fb1638244fff726dc5b36b 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -168,7 +168,7 @@ let assert_iterations m1 m2 = match m1.n, m2.n with
 
 let push m a b = 
    let a, l = match b with
-      | B.Abst _ -> {a with E.n_apix = Some m.l}, succ m.l
+      | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
       | b        -> a, m.l
    in
    let e = B.push m.e m.e a b in
@@ -179,13 +179,13 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
    match t1, r1, t2, r2 with
       | B.Sort (_, h1), _, B.Sort (_, h2), _                ->
          h1 = h2
-      | B.LRef ({E.n_apix = Some e1}, _), _, 
-        B.LRef ({E.n_apix = Some e2}, _), _                 ->
+      | B.LRef ({E.n_apix = e1}, _), _, 
+        B.LRef ({E.n_apix = e2}, _), _                      ->
         if e1 = e2 then ac_stacks st m1 m2 else false
       | B.GRef (_, u1), None, B.GRef (_, u2), None          ->
         if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
-      | B.GRef ({E.n_apix = Some e1}, u1), Some v1, 
-        B.GRef ({E.n_apix = Some e2}, u2), Some v2          ->
+      | B.GRef ({E.n_apix = e1}, u1), Some v1, 
+        B.GRef ({E.n_apix = e2}, u2), Some v2               ->
          if e1 < e2 then begin 
             if !G.summary then O.add ~gdelta:1 ();
            ac_nfs st (m1, t1, r1) (step st m2 v2)