In generalized rewrite, avoid retyping completely and constantly the conclusion, and results of

unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.

0 files changed, 0 insertions, 0 deletions