X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;h=ffe223ab5ba02de662a2eea8d134241b8b6fe2b9;hp=4a9570d50bddd96df063b1952110af714c60aee1;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 4a9570d50..ffe223ab5 100644
--- 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)                       ->