]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagReduction.ml
some interfaces improved
[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml
index 3aa576a862bb759256eb5e572a958730e347ec43..628968befdd51b7beda755cf3e322e9beae926bd 100644 (file)
@@ -26,7 +26,7 @@ type machine = {
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of B.obj
+   | GRef_ of B.entry
    | Bind_ of int * B.id * B.term * B.term
 
 type ho_whd_result =
@@ -83,8 +83,8 @@ let rec whd f c m x =
    match x with
    | B.Sort h                    -> f m (Sort_ h)
    | B.GRef uri                  ->
-      let f obj = f m (GRef_ obj) in
-      E.get_obj f uri
+      let f entry = f m (GRef_ entry) in
+      E.get_entry f uri
    | B.LRef i                    ->
       let f = function
          | B.Void   -> f m (LRef_ (i, None))