aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto3/_CoqProject
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-08 09:57:27 +0200
committerHugo Herbelin2020-04-15 19:43:28 +0200
commit79ccbe6b2b73409d7ce5e0e5797320b6e2fd0dd2 (patch)
tree64e2fa14f8343ec355284888ea4ddeb2f3e0fd45 /doc/plugin_tutorial/tuto3/_CoqProject
parentc7ed001b310583b8087574cd64ab6bed9b321f86 (diff)
Making type interning_data abstract in constrintern.ml.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/_CoqProject')
0 files changed, 0 insertions, 0 deletions