]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/basic_rg/brg.ml
ops, we forgot to update the version indicator :)
[helm.git] / helm / software / lambda-delta / src / basic_rg / brg.ml
index bc6eb57277787753485621798a8b3949597f7e92..be4e6f9b97269bfb262229981cdae00c9e167c4e 100644 (file)
@@ -16,7 +16,6 @@ module E = Entity
 module N = Level
 
 type uri = E.uri
-type id = E.id
 type attrs = E.attrs
 
 type bind = Void                   (*             *)
@@ -36,12 +35,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)
@@ -79,8 +72,3 @@ let get e i = get i e
 let rec fold_right f map e x = match e with   
    | Null              -> f x
    | Cons (e, c, a, b) -> fold_right (map f e c a b) map e x
-
-(* used in MetaBrg.unwind_to_xlate_term *)
-let rec fold_left map x = function
-   | Null              -> x
-   | Cons (e, _, a, b) -> fold_left map (map x a b) e