aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrHaskellString.v
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-09 15:08:58 +0100
committerPierre-Marie Pédrot2018-11-09 15:08:58 +0100
commit5d90e05b35f85607c43888b9adb0319e98a81fb4 (patch)
tree25787c6f6bc8ecdf601edbdacb5edb16733aaea0 /plugins/extraction/ExtrHaskellString.v
parent720a2f6e881cd2df93bc775f331c3444bebd5980 (diff)
parent46f6b27f9808848556f88032cb2af0a8a9f6c017 (diff)
Merge PR #8820: Standardize handling of Automatic Introduction.
Diffstat (limited to 'plugins/extraction/ExtrHaskellString.v')
0 files changed, 0 insertions, 0 deletions