- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[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 1a5a3f1cf47d70ac9095f00b6572d5c143d610b2..f20335193e8868dd9ed376e5be5dc8e32c46ab16 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -101,12 +101,8 @@ let rec step st m r =
       else m, r, None
    | B.GRef (_, uri)                     ->
       begin match BE.get_entity uri with
-         | _, _, _, E.Abbr v ->
-            if !G.expand then begin
-              if !G.summary then O.add ~gdelta:1 ();
-               step st m v
-            end else
-              m, r, Some v
+         | _, a, _, E.Abbr v ->
+              m, B.gref a uri, Some v
          | _, _, _, E.Abst w ->
             if assert_tstep m true then begin
                if !G.summary then O.add ~grt:1 (); 
@@ -126,7 +122,7 @@ let rec step st m r =
                if !G.summary then O.add ~lrt:1 ();
                step st {(tstep m) with e = c} w
             end else
-              m, B.LRef (a, i), None
+              m, B.lref a i, None
         | _, _, B.Void           ->
            assert false
       end