X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2Fbag.ml;h=b04fc5ab6aa84edc4be107a60cb8dca852f0e7ab;hb=4dc87cc7384ba61136bc82a23effe6a52160e720;hp=d0c193a2a71a0ad4528d21952320ae93ea022181;hpb=338e3e5c639fbcfeeb347a0121cacc6c0f1fc42a;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml
index d0c193a2a..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
 
@@ -55,11 +58,19 @@ let location = ref 0
 
 let new_location () = let loc = !location in incr location; loc
 
+let locations () = !location
+
 (* context handling functions ***********************************************)
 
 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 =