aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-11-08 10:27:53 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-11-08 10:27:53 -0500
commit420a7c968214a797141c03f1ec24b20100645b60 (patch)
treea4f8875f1758ad52c446ecc46bb2f1b01732e99f /src/Util/Tuple.v
parentc8857ab685ea40af6781fd201d258610ed9326f2 (diff)
Work around bug 5189 (broken [Hint Resolve ->])
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5189, [Hint Resolve <- foo] does not survive the end of modules
Diffstat (limited to 'src/Util/Tuple.v')
0 files changed, 0 insertions, 0 deletions