]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgUntrusted.ml
- conditional compilation continues ...
[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml
index d6333552f59e520a85075b2b3200afa64b7fff18..a6ab35ea94420b3d2f03ffd619512a53afcc4321 100644 (file)
@@ -20,6 +20,8 @@ module BV = BrgValidity
 
 (* Interface functions ******************************************************)
 
+IFDEF TYPE THEN
+
 (* to share *)
 let type_check err f st = function
    | ra, na, uri, E.Abst t ->
@@ -40,6 +42,8 @@ let type_check err f st = function
       BT.type_of err f st BR.empty_rtm t
    | _, _, _, E.Void       -> assert false
 
+END
+
 let validate err f st e =
    let uri, t = match e with
       | _, _, uri, E.Abst t -> uri, t