aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorJasper Hugunin2019-01-06 20:29:19 -0800
committerJasper Hugunin2019-02-04 11:38:04 -0800
commit735d3fd21c65688143541d77c4153f52b963f4c4 (patch)
treef63d7856f47c7cf6cf4a4d43f515460fba9936a9 /dev/include
parent5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff)
Enrich implicits for instances
For compatibility, also * Adjust implicits on equiv_transitivity and equiv_symmetry, and in some closed bugs * Add overlay for HoTT setting Arguments on some instances.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions