]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguateTypes.ml
Big commit and major code clean-up:
[helm.git] / helm / ocaml / cic_disambiguation / disambiguateTypes.ml
index 292d78e4b1bbbaf8ad4c0c582b7221ce404ab075..078297a26e966739f12eac162de6cc0b49a5525b 100644 (file)
@@ -50,6 +50,12 @@ type codomain_item =
 
 and environment = codomain_item Environment.t
 
+(** adds a (name,uri) list l to a disambiguation environment e **)
+let env_of_list l e = 
+  List.fold_left
+   (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e)
+   e l
+
 module type Callbacks =
   sig
     val interactive_user_uri_choice: