diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-30 15:55:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-30 15:55:24 +0200 |
| commit | 1ee23d71dadd6211c36afe8d2891b7170535cd62 (patch) | |
| tree | af9b5b1cdf72d0cc410e64959727950c60a270bd /theories/Reals/Rprod.v | |
| parent | 63ecb7386ae6e705d3f5577e01ec543f706c9427 (diff) | |
Followup of 9f81b58551.
The hash function exported by the interface ought to respect the equality.
Therefore, we only use the syntactic hash for the hashconsing module while
using the canonical hash in the API.
Diffstat (limited to 'theories/Reals/Rprod.v')
0 files changed, 0 insertions, 0 deletions