-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
- (fun aid sid args acic2cexpr ->
- match (List.tl args) with
- [Cic.ALambda (_,Cic.Name n,s,t)] ->
- Binder
- (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
- | _ -> raise Not_found);;
-
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"