diff options
author | 2016-10-29 15:42:59 +0200 | |
---|---|---|
committer | 2016-10-29 15:42:59 +0200 | |
commit | b5d88066acbcebf598474e0d854b16078f4019ce (patch) | |
tree | 21ff55b88150d6326a70411d720075f8ad4b93df /test-suite/bugs/closed | |
parent | b3a57e84241c40915169aa410f5606175cf609be (diff) | |
parent | 9c0bec7cb273ec00be45bfe728f87150c3d2f925 (diff) |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'test-suite/bugs/closed')
-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. |