(** 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)));