Composite coercions are here!

[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 d0c193a2a71a0ad4528d21952320ae93ea022181..b04fc5ab6aa84edc4be107a60cb8dca852f0e7ab 100644 (file)
--- 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 =