update in helena

[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 4a9570d50bddd96df063b1952110af714c60aee1..ffe223ab5ba02de662a2eea8d134241b8b6fe2b9 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -105,9 +105,9 @@ ELSE () END;
       else m, r, None
    | B.GRef (_, u)                       ->
       begin match BE.get_entity u with
-         | _, a, _, E.Abbr v ->
+         | _, a, _, E.Abbr (_, v) ->
               m, B.gref a u, Some v
-         | _, _, _, E.Abst w ->
+         | _, _, _, E.Abst (_, w) ->
             if assert_tstep m true then begin
 IFDEF SUMMARY THEN
                if !G.summary then O.add ~grt:1 ()
@@ -115,7 +115,7 @@ ELSE () END;
                step st (tstep m) w
             end else
               m, r, None   
-        | _, _, _, E.Void   ->
+        | _, _, _, E.Void        ->
             assert false
       end
    | B.LRef (_, i)                       ->