Mentions légales du service

Skip to content

Fix bug #456

Guillaume Melquiond requested to merge fix_456 into master

This reduces the time spent in Term.t_compare and Term.t_hash. On #456 (closed), time is divided by four.

A further 30% improvement can be obtained by disabling the computation of unknown identifiers in Decl.d_node for goal declarations, but the change is deemed too unsafe by @paskevyc and I. (Transformations would have to be careful that goals contain only known identifiers.)

Merge request reports