diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-21 17:35:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-21 17:41:58 +0200 |
| commit | 2192f5a2ccedd5e761380f4ef8464236379d4d4a (patch) | |
| tree | 9126b8e724f03ea9b0a11c908f704ad45804e6f0 /plugins/cc/g_congruence.ml4 | |
| parent | be6f66e3d4424b0dfbbbe3097a617aebb8aefca2 (diff) | |
Inline a function from Quote used in setoid_ring.
The code was wrong as it relies once again on term equality and fails
on polymorphic constants. Quote is bound to disappear, so we write a
correct version of this 10-line function in setoid_ring.
Diffstat (limited to 'plugins/cc/g_congruence.ml4')
0 files changed, 0 insertions, 0 deletions