let (proof, goal) =
prerr_endline "a2";
(match CicParser.obj_of_xml tmp1 (Some tmp2) with
- | Cic.CurrentProof (_,metasenv,bo,ty,_) -> (* TODO il primo argomento e' una URI valida o e' casuale? *)
+ | Cic.CurrentProof (_,metasenv,bo,ty,attrs) -> (* TODO il primo argomento e' una URI valida o e' casuale? *)
prerr_endline "a3";
let uri = UriManager.uri_of_string "cic:/foo.con" in
prerr_endline "a4";
typecheck_loaded_proof metasenv bo ty;
prerr_endline "a5";
- ((uri, metasenv, bo, ty), goal)
+ ((uri, metasenv, bo, ty, attrs), goal)
| _ -> assert false)
in
prerr_endline "a6";