X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.ml;h=368bc2f45f9a21911821ba9ffbd905a37c542ad7;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=c74566f20861c4e030621d6b49c0cf642cb1726b;hpb=45586ab88c026e6a21927654387b6df266a44700;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index c74566f20..368bc2f45 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
@@ -84,10 +84,15 @@ 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, []));
+  add_symbol_choice "cast"
+    ("type cast",
+      (fun env _ args ->
+        let t1, t2 =
+          match args with 
+          | [t1; t2] -> t1, t2
+          | _ -> raise Invalid_choice
+        in
+        Cic.Cast (t1, t2)));