Skip to content

Forall notation changes to type scope unlike builtin syntax

@gmalecha MR !152 (merged) broke something in Perennial because it caused * to be interpreted in type scope instead of Z. Coq's Unicode ∀ notation does not put the argument in type scope (and indeed it should be unnecessary because the whole notation is in type scope), so probably the override shouldn't either: https://github.com/coq/coq/blob/master/theories/Unicode/Utf8_core.v#L15.