X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.ml;h=749e9148b979e7d7a137fef76f4968f556767afb;hb=8caaccfeb66f6a507e5fb3b4b221a360eb5428c8;hp=b6ae4e6beeed373ec00f7aaac2cb9c62c6674371;hpb=ea6b99ed26a954a578e3c88909479dcf9cab7345;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml
index b6ae4e6be..749e9148b 100644
--- a/helm/ocaml/cic_notation/cicNotationEnv.ml
+++ b/helm/ocaml/cic_notation/cicNotationEnv.ml
@@ -50,6 +50,8 @@ let lookup_value env name =
     snd (List.assoc name env)
   with Not_found -> raise (Value_not_found name)
 
+let remove env name = List.remove_assoc name env
+
 let lookup_term env name =
   match lookup_value env name with
   | TermValue x -> x
@@ -100,3 +102,22 @@ let rec well_typed ty value =
       List.for_all (fun value' -> well_typed ty' value') vl
   | _ -> false
 
+let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty))
+
+let coalesce_env declarations env_list =
+  let env0 = List.map list_binding_of_name declarations in
+  let grow_env_entry env n v =
+    List.map
+      (function
+        | (n', (ty, ListValue vl)) as entry ->
+            if n' = n then n', (ty, ListValue (v :: vl)) else entry
+        | _ -> assert false)
+      env
+  in
+  let grow_env env_i env =
+    List.fold_left
+      (fun env (n, (_, v)) -> grow_env_entry env n v)
+      env env_i
+  in
+  List.fold_right grow_env env_list env0
+