aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/README.md
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-15 16:11:29 +0000
committerGitHub2020-11-15 16:11:29 +0000
commit93ee64000d4e121718b4735468626b481b2533bc (patch)
treedd7fdfb6a7b1e2a41fc55fb811d8ea234862bbfb /doc/plugin_tutorial/README.md
parent010dfd516839b901ce8e69dffc0c3751564a8ad6 (diff)
parent3687c3fdcf2edd7b8e7f7408d9a8ee8706fd16a9 (diff)
Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly
Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions