]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/metaBag.ml
rewritten instantiate code
[helm.git] / helm / software / lambda-delta / toplevel / metaBag.ml
index 4f909bdcaa00443832415fae696f4e104f0658c1..67c938df0db267acc84f972b4c331ff93a62ee58 100644 (file)
@@ -45,7 +45,7 @@ let xlate_pars f pars =
       let f w = B.push "meta" f c l id (B.Abst w) in
       xlate_term c f w
    in
-   C.list_fold_right f map pars B.empty_context
+   C.list_fold_right f map pars B.empty_lenv
 
 let unwind_to_xlate_term f c t =
    let map f t (l, id, b) = f (B.bind l id b t) in
@@ -63,10 +63,10 @@ let xlate_entry f = function
       let f c = unwind_to_xlate_term (f c) c u in
       xlate_pars f pars
 
-let xlate_item f = function
+let xlate_entity f = function
    | None   -> f None
    | Some e -> let f e = f (Some e) in xlate_entry f e
 
 (* Interface functions ******************************************************)
 
-let bag_of_meta = xlate_item
+let bag_of_meta = xlate_entity