]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/complete_rg/crg.ml
when sort inclusion is enabled, we can produce conversion constraints in xml
[helm.git] / helm / software / lambda-delta / src / complete_rg / crg.ml
index d272bdea8c41d6e3cd366aada1f079467b301407..9020048af077f7f8e95f7797afc5188b3887fb47 100644 (file)
@@ -39,10 +39,6 @@ type entity = term E.entity
 
 (* helpers ******************************************************************)
 
-let mk_uri si root s =
-   let kernel = if si then "crg-si" else "crg" in
-   String.concat "/" ["ld:"; kernel; root; s ^ ".ld"]
-
 let empty_lenv = ESort
 
 let push_bind f lenv a b = f (EBind (lenv, a, b))