P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
cexpr2pres a;P.Mtext([],")")])));
+(* inv *)
+Hashtbl.add C2P.symbol_table "inv" (unary
+ (fun a ~priority ~assoc ~tail attr sattr ->
+ P.Msup([],
+ P.Mrow([],[
+ P.Mtext([],"(");
+ cexpr2pres a;
+ P.Mtext([],")")]),
+ P.Mrow([],[
+ P.Mo([],"-");
+ P.Mn([],"1")]))));
+
+(* opp *)
+Hashtbl.add C2P.symbol_table "opp" (unary
+ (fun a ~priority ~assoc ~tail attr sattr ->
+ P.Mrow([],[
+ P.Mo([],"-");
+ P.Mtext([],"(");
+ cexpr2pres a;
+ P.Mtext([],")")])));
+
(* leq *)
Hashtbl.add C2P.symbol_table "leq" (binary
(fun a b ~priority ~assoc ~tail aattr sattr ->
None, Some "cic:/Coq/Init/Logic/not.con"))
:: List.map acic2cexpr args));;
+(* Rinv *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "inv",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+ :: List.map acic2cexpr args));;
+
+(* Ropp *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "opp",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+ :: List.map acic2cexpr args));;
+
(* exists *)
Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->