Set( prologoutput, 2 ). Set( totalproof, 1 ).If a proof is found, then the part between the strings
% ABCDEFGHIJKLMNOPQRSTUVWXYZshould be read by translate.pro . There is currently no tool to extract the relevant part from the proof, this has to be done by hand in an editor. Inside Eclipse, type
['translate.pro']. translate( 'File1', 'File2' ).File1 is the name of the output of Bliksem. File2 is the file in which the translation will be written.
linecut < File2 > File3
['tt.pro']. include( 'File3' ).
['coq.pro']. translate( 'File3', 'File4' ).The output has to be cut again by linecut.c , resulting in File5. File5 can be entered into Coq by cut-and-paste, or by typing
Load File5.inside Coq.