aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqdecide.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-03 19:43:03 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-03 19:43:03 +0200
commit14a50277b58eae50f14f7dea965dec7f8bc416a3 (patch)
tree6862b30edd5ce0475c8fa1b8c5816663ebe918c1 /tactics/eqdecide.ml
parente4c9f490a588424a49cb092ce38ad757f5c6e712 (diff)
parent6deddd3e0c6cc1d7cbf8414f7553c5d7752a0801 (diff)
Merge PR#588: Allow interactive editing of {C,}Morphisms in PG
Diffstat (limited to 'tactics/eqdecide.ml')
0 files changed, 0 insertions, 0 deletions