Thibault Gauthier

@xrchz Can you please provide an example proof that would benefit from a ((goal,tactic (string)),(input,output)) cache? Encapsulating `e` with a recorder and replayer seems the least invasive way of doing...

I am not sure I understand the problem correctly. If the effect of the long-lasting tactic is known, why not just replace it by a tactic that maps its input...

I have implemented parmap (parallel map) in tttTools using PolyML. Unfortunately, Metis is not robust to parallelism and return a Subscript error when run in parallel. > load "tttTools"; val...

Most of the exception won't use these fields. So there might be a negligible amount of a (memory/cpu) waste. Could you provide motivating examples that require these changes?

Indeed term_to_string is slow. I understand the reason now.