X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagReduction.ml;h=b7eb88f6395ee4f3fd0a5dbb24f4d6d9450b8907;hb=4c157ac5c58f34fffc98289c2d2e71032d584a83;hp=628968befdd51b7beda755cf3e322e9beae926bd;hpb=79684e8bd0f54b5c88fff981366bd8c78dd0fbe9;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index 628968bef..b7eb88f63 100644
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -12,6 +12,7 @@
 module U = NUri
 module C = Cps
 module L = Log
+module Y = Entity
 module B = Bag
 module O = BagOutput
 module E = BagEnvironment
@@ -26,7 +27,7 @@ type machine = {
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of B.entry
+   | GRef_ of B.entity
    | Bind_ of int * B.id * B.term * B.term
 
 type ho_whd_result =
@@ -84,7 +85,7 @@ let rec whd f c m x =
    | B.Sort h                    -> f m (Sort_ h)
    | B.GRef uri                  ->
       let f entry = f m (GRef_ entry) in
-      E.get_entry f uri
+      E.get_entity f uri
    | B.LRef i                    ->
       let f = function
          | B.Void   -> f m (LRef_ (i, None))
@@ -116,10 +117,10 @@ let rec ho_whd f c m x =
       | Bind_ (_, _, w, _)     -> 
          let f w = f (Abst w) in unwind_to_term f m w
       | LRef_ (_, Some w)      -> ho_whd f c m w
-      | GRef_ (_, _, B.Abst w) -> ho_whd f c m w  
-      | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v
+      | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w  
+      | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
       | LRef_ (_, None)        -> assert false
-      | GRef_ (_, _, B.Void)   -> assert false
+      | GRef_ (_, _, Y.Void)   -> assert false
    in
    whd aux c m x
    
@@ -139,9 +140,11 @@ let rec are_convertible f ~si 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 ~si a c m1 m2 else f false
-      | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _)   ->
+      | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _), 
+        GRef_ ((Y.Apix a2 :: _), _, Y.Abst _)              ->
          if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
-      | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
+      | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1), 
+        GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2)             ->
          if a1 = a2 then
 	    let f a = 
 	       if a then f a else are_convertible f ~si true c m1 v1 m2 v2
@@ -150,9 +153,9 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 =
 	 else
 	 if a1 < a2 then whd (aux m1 r1) c m2 v2 else
 	 whd (aux_rev m2 r2) c m1 v1
-      | _, GRef_ (_, _, B.Abbr v2)                         ->
+      | _, GRef_ (_, _, Y.Abbr v2)                         ->
          whd (aux m1 r1) c m2 v2
-      | GRef_ (_, _, B.Abbr v1), _                         ->
+      | GRef_ (_, _, Y.Abbr v1), _                         ->
 	 whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2)   ->
 	   let l = B.new_location () in