- static disambiguation of Automath unified binders

[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 f397c1c6f5c10ceac594ed4617ff6a164757b836..c0ff7757552962f150acba8c17f29493f01391c5 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -205,9 +205,11 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
       | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->
-(*         if N.is_zero n then () else Q.add_zero st.S.cc a; *)
-        if !G.summary then O.add ~si:1 ();
-        ac st (push m1 a b) t1 (push m2 a b) t
+         if st.S.si then begin
+(*       if N.is_zero n then () else Q.add_zero st.S.cc a; *)
+           if !G.summary then O.add ~si:1 ();
+           ac st (push m1 a b) t1 (push m2 a b) t
+         end else false
       | _                                                   -> false
 
 and ac st m1 t1 m2 t2 =