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

[helm.git] / helm / software / helena / src / basic_ag / bagReduction.ml

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index fd564e83e744575a0bcb84db9f64c5b1c4838d76..513c14e59240a3cf6a710d95194b1b0652afee06 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -139,11 +139,11 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
          if h1 = h2 then f a else f false 
       | LRef_ (i1, _), LRef_ (i2, _)                       ->
          if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ (_, {E.n_apix = Some a1}, _, E.Abst _), 
-        GRef_ (_, {E.n_apix = Some a2}, _, E.Abst _)       ->
+      | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), 
+        GRef_ (_, {E.n_apix = a2}, _, E.Abst _)            ->
          if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ (_, {E.n_apix = Some a1}, _, E.Abbr v1), 
-        GRef_ (_, {E.n_apix = Some a2}, _, E.Abbr v2)      ->
+      | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), 
+        GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2)           ->
          if a1 = a2 then
            let f a = 
               if a then f a else are_convertible f st true c m1 v1 m2 v2