-(* logical operators *)
-
-interpretation "logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
-interpretation "logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
-interpretation "logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
-interpretation "exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y).
-
-(*
- 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)));
-*)
-