we corrected some reduction bugs about renaming.

[helm.git] / helm / software / lambda-delta / basic_ag / bag.ml

diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml
index 0ca3140151d4e5eefaa3f0d90aa92eec43d0ab5f..624b47cbb38e1106f78725524126cf2bbc73e793 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bag.ml
+++ b/helm/software/lambda-delta/basic_ag/bag.ml
@@ -61,7 +61,13 @@ let locations () = !location
 
 let empty_context = []
 
-let push f es l id b =
+let push msg f es l id b =
+   let rec does_not_occur loc = function
+      | []                          -> true
+      | (l, _, _) :: _ when l = loc -> false
+      | _ :: es                     -> does_not_occur l es
+   in
+   if not (does_not_occur l es) then failwith msg else
    let c = (l, id, b) :: es in f c
 
 let append f es1 es2 =