eq_expr called from leq_ordinal could use the pool oracle (mantis #54)

rlepigre / pml

New version of the PML language and (classical) proof assistant

http://pml-lang.org

MIT License

20 stars 2 forks source link

Closed craff closed 6 years ago

craff commented 6 years ago

When 0000032 is solved, we will know ...

Does not seem usefull.

craff commented 6 years ago

Yes, really useless or done