X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2Fbag.ml;h=b04fc5ab6aa84edc4be107a60cb8dca852f0e7ab;hb=db7f6d6b32515c091e0f338dd4903624f35f27ac;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..b04fc5ab6 100644
--- a/helm/software/lambda-delta/basic_ag/bag.ml
+++ b/helm/software/lambda-delta/basic_ag/bag.ml
@@ -9,6 +9,9 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+(* kernel version: basic, absolute, global *)
+(* note          : experimental *) 
+
 type uri = NUri.uri
 type id = Aut.id
 
@@ -61,7 +64,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 =