diff options
| author | Hugo Herbelin | 2020-09-03 11:44:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-03 11:44:40 +0200 |
| commit | 8cd66c83327093ec90f8b7d489cd4bd62d92e5f2 (patch) | |
| tree | 60ece61b3b9f8614283c81405fdaedca4e168cdb /kernel/term.ml | |
| parent | ce0c1475badd3ceef940db1fab965128cd752e6a (diff) | |
| parent | 93ac07bbb48ba3a2eca0d5c75aa9be7095a19912 (diff) | |
Merge PR #12973: Random cleanup around the data structures used in Equality
Reviewed-by: herbelin
Diffstat (limited to 'kernel/term.ml')
0 files changed, 0 insertions, 0 deletions