Mentions légales du service

Skip to content

separate transformations for intros, dequant, and remove_unused

MARCHE Claude requested to merge real_trans_for_removing_ce_symbols into master

This MR should resolve the problem of unused symbols seen in the IDE, and also the regressions on proofs due to too many extra symbols.

Merge request reports