when sort inclusion is enabled, we can produce conversion constraints in xml

[helm.git] / helm / software / lambda-delta / src / basic_rg / brgType.ml

diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml
index 2bead2d3344b3237f96ad71c6c5cc048cb1c5cdb..f23da87d09fad4304838ccff99d8c5420756b5ae 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgType.ml
@@ -11,7 +11,7 @@
 
 module U  = NUri
 module C  = Cps
-module S  = Share
+module W  = Share
 module L  = Log
 module H  = Hierarchy
 module E  = Entity
@@ -88,7 +88,7 @@ let rec b_type_of err f st m x =
       end
    | B.Bind (a, B.Abbr v, t) ->
       let f xv xt tt =
-         f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+         f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
       in
       let f xv m = b_type_of err (f xv) st m t in
       let f xv = f xv (BR.push m a (B.abbr xv)) in
@@ -99,27 +99,27 @@ let rec b_type_of err f st m x =
       type_of err f st m v
    | B.Bind (a, B.Abst (n, u), t) ->
       let f xu xt tt =
-        f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
+        f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
       in
       let f xu m = b_type_of err (f xu) st m t in
       let f xu _ = f xu (BR.push m a (B.abst n xu)) in
       type_of err f st m u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
-         f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+         f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
       in
       b_type_of err f st (BR.push m a B.Void) t
          
    | B.Appl (a, v, t)        ->
       let f xv vv xt tt = 
-         let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+         let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
          assert_applicability err f st m tt vv xv
       in
       let f xv vv = b_type_of err (f xv vv) st m t in
       type_of err f st m v
    | B.Cast (a, u, t)        ->
       let f xu xt tt =  
-        let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in
+        let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in
          assert_convertibility err f st m xu tt xt
       in
       let f xu _ = b_type_of err (f xu) st m t in