aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-06-23 17:02:50 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-06-26 16:26:29 +0200
commit3e0aa07cfb1d552e11b37aaf5f0224bfb5b47523 (patch)
tree4bc6b6da094ce285ba5f8a967875e6731b1dd971 /toplevel/coqinit.mli
parentef6459b00999a29183edc09de9035795ff7912e9 (diff)
BUGFIX: Three fixes for the price of 1 in sorts.ml:
- Proper [family] implementation - Use the tailor made hash function for Sorts.t in two places.
Diffstat (limited to 'toplevel/coqinit.mli')
0 files changed, 0 insertions, 0 deletions