aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-07 03:45:27 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-12 16:49:46 +0200
commitb63b9a86b09856262b5b7bb2b3bb01f704032d41 (patch)
treeb7480e3d41a1dd418c98f73034fc907df1ffbcac /ide/coqOps.ml
parentcf24cedb2926fa00db222eeac48e88a6078b4444 (diff)
[toplevel] [stm] cleanup in module open
Diffstat (limited to 'ide/coqOps.ml')
0 files changed, 0 insertions, 0 deletions