added cast concrete syntax

[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 9caf77aabf0618bdac3f2071a056a569d2398ff7..368bc2f45f9a21911821ba9ffbd905a37c542ad7 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
@@ -85,4 +85,14 @@ let lookup_num_by_dsc dsc =
 
 let _ =
   add_binary_op "exists" "exists"
-   (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []))
+    (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)));
+