aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-05-04 12:07:10 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-05-04 12:07:10 +0200
commit8af2e5223dfe84c87d7943c2db0cd6b62e8a4635 (patch)
tree03647f1572cba0a410f2292d9b92db86d228671a /ide/ideutils.ml
parent796859aca4fc85dc721b670d95b0c2aaace55e32 (diff)
parent5b4e3ace20eb2ab569d172a1f358f26f451d361c (diff)
Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq into v8.5
Diffstat (limited to 'ide/ideutils.ml')
0 files changed, 0 insertions, 0 deletions