Commit 4a85888c authored by Ralf Jung's avatar Ralf Jung
Browse files

disable some notation for now

parent 1d11aac6
......@@ -1454,5 +1454,9 @@ Section sigTOF.
End sigTOF.
Arguments sigTOF {_} _%OF.
FIXME: Notation disabled because it causes strange conflicts in Coq 8.7.
Enable again once we drop support for that version.
Notation "{ x & P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
Notation "{ x : A & P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment