]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/basic_rg/brg.ml
when sort inclusion is enabled, we can produce conversion constraints in xml
[helm.git] / helm / software / lambda-delta / src / basic_rg / brg.ml
index bc6eb57277787753485621798a8b3949597f7e92..0386523091c059e828b02ceed2e86d3e0ca62623 100644 (file)
@@ -36,12 +36,6 @@ type lenv = Null
 (* Cons: tail, relative local environment, attrs, binder *) 
           | Cons of lenv * lenv * attrs * bind 
 
-(* helpers ******************************************************************)
-
-let mk_uri si root s =
-   let kernel = if si then "brg-si" else "brg" in
-   String.concat "/" ["ld:"; kernel; root; s ^ ".ld"]
-
 (* Currified constructors ***************************************************)
 
 let abst n w = Abst (n, w)