diff options
| author | Brian Campbell | 2019-10-02 16:44:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-10-02 16:44:56 +0100 |
| commit | 2374aea33aa332f3927dd4dc4d6d9a15f5620ac9 (patch) | |
| tree | e84accdd464868a9ece9971ca17a2bae45aa62d6 /src/util.ml | |
| parent | 2d1051cc4a1dfdd1a55e2df6ba331d7f1954bb61 (diff) | |
Coq: generate decidable equality instances for variant types
It only produces them when necessary (because some types do not have
decidable equality due to embedded proofs).
Also add trivial instance for the unit type.
Diffstat (limited to 'src/util.ml')
0 files changed, 0 insertions, 0 deletions