aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrHaskellString.v
diff options
context:
space:
mode:
authorGaƫtan Gilbert2019-05-05 16:42:36 +0200
committerEnrico Tassi2019-06-04 09:33:41 +0200
commit33b18aaffd999fb6d31fd5e9c7ca4426d5186983 (patch)
tree0b0f5efeb5e9cbe2fb3eabaff058e25cf4b5eac9 /plugins/extraction/ExtrHaskellString.v
parent1bf2a088387949c13602997d181e6f7d0f014b3f (diff)
instance_name grammar entry isn't global
Not needed since we don't allow anonymous Declare Instance anymore (was needed for factorization or some such before that I think)
Diffstat (limited to 'plugins/extraction/ExtrHaskellString.v')
0 files changed, 0 insertions, 0 deletions