Partial porting to V8 URIs.

[helm.git] / helm / ocaml / cic_disambiguation / disambiguateChoices.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index c74566f20861c4e030621d6b49c0cf642cb1726b..9caf77aabf0618bdac3f2071a056a569d2398ff7 100644 (file)
--- 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, []))