aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-16 18:55:58 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-16 19:12:37 +0200
commit73c153101b8b7ccc0c279161869265b596032b0e (patch)
tree1da4ddc7fd1f090722debe97b5461629531e8bbd /printing
parent951e508dc1fafd6788821a5a80c1b4759c81ae29 (diff)
Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,
fix the type of the term which has to be in the signature of the evar to declare); some problems remain though (see next commit).
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions