The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello all,

Here is a simplified example of what I am trying to do.

Require Import QArith.

Parameter bla: nat -> nat -> Prop.

Notation "A ~ B" := (bla A B) (at level 70).

Parameter bla_equal:
   forall c: nat,
   c ~ c.

Coq (version 8.3pl2) reacts to the last line by saying "Syntax error: '0' or '1' expected after '~' (in [constr:operconstr])".

Apparently this is due to the fact that because of the QArith import a notation that involves "~" is defined. I tried various ways of getting around this. E.g., trying "Close Scope positive", trying to put my notation in a scope and opening that and so forth. None of this seems to help. Any ideas?

All the best,
Chris