X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.ml;h=9caf77aabf0618bdac3f2071a056a569d2398ff7;hb=b3bfd6b249600b15552c890306a635aee30c2a74;hp=c74566f20861c4e030621d6b49c0cf642cb1726b;hpb=ba2709d8c270e7f6ffbdb8bd3a192bc071407f03;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index c74566f20..9caf77aab 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
@@ -84,10 +84,5 @@ let lookup_num_by_dsc dsc =
   (** initial table contents *)
 
 let _ =
-  let uri s = UriManager.uri_of_string s in
-  let const s = Cic.Const (uri s, []) in
-  let mutind s = Cic.MutInd (uri s, 0, []) in
-  add_binary_op "exists" "exists" (mutind "cic:/Coq/Init/Logic/ex.ind");
-  add_binary_op "exists" "exists over terms with sort Type"
-    (mutind "cic:/Coq/Init/Logic_Type/exT.ind");
-
+  add_binary_op "exists" "exists"
+   (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []))