]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/complete_rg/crgBrg.ml
Splitted gpts in two files.
[helm.git] / helm / software / lambda-delta / complete_rg / crgBrg.ml
index d07e6efbf7730331bea330ec2520f7acaa74c660..bfed7ad9e7174d65c536c905fcb65e6ca1f113a3 100644 (file)
@@ -45,16 +45,16 @@ and xlate_bind x a b =
    match b with
       | D.Abst ws ->
          let map x n w = 
-           let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
+           let f ww = B.Bind (n :: a, B.Abst ww, x) in xlate_term f w
         in
         List.fold_left2 map x ns ws 
       | D.Abbr vs ->
          let map x n v = 
-           let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f v
+           let f vv = B.Bind (n :: a, B.Abbr vv, x) in xlate_term f v
         in
         List.fold_left2 map x ns vs
       | D.Void _  ->
-         let map x n = B.Bind (B.Void (n :: a), x) in
+         let map x n = B.Bind (n :: a, B.Void, x) in
         List.fold_left map x ns
 
 and xlate_proj x _ e =