[Hol-info] EmitTeX.print_theories_as_tex_doc can't overwrite existing files

[Chun Tian (binghe)]

Hi,

When I use EmitTeX.print_theories_as_tex_doc to export theories into TeX 
documents, if the target TeX files already exist, the command reports HOL_ERR:

File ../papers/references already exists.
Exception-
   HOL_ERR
     {message = "File exists", origin_function = "failwith",
      origin_structure = "??"} raised

This doesn’t make any sense, I think, as other commands like DB.html_theory () 
does allow overwriting files.

Is there any hidden option that allows me to call 
EmitTeX.print_theories_as_tex_doc without deleting existing files first?

Regards,

Chun Tian

signature.asc
Description: Message signed with OpenPGP using GPGMail

------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info