Viewing all changes in revision 18513.
- Committer: Hugo Herbelin
- Date: 2016-10-27 17:23:16 UTC
- Revision ID: git-v1:9c0bec7cb273ec00be45bfe728f87150c3d2f925
Fixing #5161 (case of a notation with unability to detect a recursive binder).
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
- files added:
- test-suite/bugs/closed/5161.v
- files modified:
- interp/notation_ops.ml
expand all
collapse all
added
removed
