New function [Constr.equal_with] to compare terms up to variants of [kind_of_term].

To be able to write equality up to evar instantiation instantiation.

Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.

0 files changed, 0 insertions, 0 deletions