diff options
author | 2016-10-27 19:17:37 +0200 | |
---|---|---|
committer | 2016-10-27 19:23:16 +0200 | |
commit | 9c0bec7cb273ec00be45bfe728f87150c3d2f925 (patch) | |
tree | b709d950c71640819377d46ad181ee38d75573a9 /test-suite/bugs | |
parent | 2290dbb9c95b63e693ced647731623e64297f5c8 (diff) |
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.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/5161.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v new file mode 100644 index 000000000..d28303b8a --- /dev/null +++ b/test-suite/bugs/closed/5161.v @@ -0,0 +1,27 @@ +(* Check that the presence of binders with type annotation do not + prevent the recursive binder part to be found *) + +From Coq Require Import Utf8. + +Delimit Scope C_scope with C. +Global Open Scope C_scope. + +Delimit Scope uPred_scope with I. + +Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x. + +Notation "∀ x .. y , P" := + (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. +Infix "∧" := and : uPred_scope. + +(* The next command fails with + In recursive notation with binders, Φ is expected to come without type. + I would expect this notation to work fine, since the ∀ does support + type annotation. +*) +Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := + (∀ Φ : _ → _, + (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I + (at level 20, x closed binder, y closed binder, + format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. |