]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgCrg.ml
- siimplifified RTM (one register less) now counts x-steps.
[helm.git] / helm / software / helena / src / basic_rg / brgCrg.ml
index 0fcde12aa4bcefb0603ca02debe71e32fa0134e8..dd7f3b1e597d9d0e16b15aa0d661c0cf6f05bcf9 100644 (file)
@@ -36,7 +36,7 @@ let rec xlate_term f = function
 
 and xlate_bind f a b x = match b with
    | D.Abst (n, w) ->
-      let f ww = f (B.Bind (a, B.Abst (n, ww), x)) in 
+      let f ww = f (B.Bind (a, B.Abst (false, n, ww), x)) in 
       xlate_term f w
    | D.Abbr v      ->
       let f vv = f (B.Bind (a, B.Abbr vv, x)) in 
@@ -64,13 +64,13 @@ let rec xlate_bk_term f = function
       xlate_bk_term f t 
 
 and xlate_bk_bind f = function
-   | B.Abst (n, t) ->
+   | B.Abst (_, n, t) ->
       let f tt = f (D.Abst (n, tt)) in
       xlate_bk_term f t
-   | B.Abbr t      ->
+   | B.Abbr t         ->
       let f tt = f (D.Abbr tt) in
       xlate_bk_term f t
-   | B.Void        -> f D.Void
+   | B.Void           -> f D.Void
    
 (* interface functions ******************************************************)