]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgType.ml
improved type hierarchy management
[helm.git] / helm / software / lambda-delta / basic_rg / brgType.ml
index fd240994543168287d2c42353561d664d36c3171..50d20b7546b89a0b94e1cb96e27d65a5ce976fec 100644 (file)
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 module L = Log
+module H = Hierarchy
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
@@ -32,7 +33,8 @@ let error2 s1 c1 t1 s2 c2 t2 =
 let rec type_of f g c x = 
    L.log O.specs level (L.ct_items1 "now checking" c x);
    match x with
-   | B.Sort h                 -> f (B.Sort (g h))
+   | B.Sort h                 ->
+      let f h = f (B.Sort h) in H.apply f g h
    | B.LRef i                 ->
       let f = function
          | Some (_, B.Abst w)               -> f w