EmilieGrienenberger

The issue is that proofs are shared between main theorems, so some intermediate steps of the proofs are defined as theorems by themselves. In a file containing the proofs of...

Thank you for your quick answers. However, I already use the thm keyword. I will try to make my issue clearer with an example. The generated dk files may look...

Exactly, I would only need addition1 and addition2 to be recorded in the object file. I have more than 300 files of generated proofs (total of a bit less than...

I did some tests. - The thm keyword works : I tried using the def keyword to define my theorems, the dko files are as expected heavier. - It explodes...

@rlepigre I have no guarantee that an intermediate theorem is not used in two different main theorems. A way to get around this would be to directly generate one file...

I uploaded the files on my directory in the deducteam InriaForge repo (deducteam/member/grienenberger/). It should be a good version, don't hesitate to tell me if there is an issue.