X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2Fbag.ml;h=624b47cbb38e1106f78725524126cf2bbc73e793;hb=421056da7b3e1d6b9d91d72092b4f3c3232a00ce;hp=0ca3140151d4e5eefaa3f0d90aa92eec43d0ab5f;hpb=426005acf6fb05116de5bae20591eefe55a4df00;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml
index 0ca314015..624b47cbb 100644
--- 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 =