Coq: Définition d'une notation de préfixe

Question

J'ai essayé w/différents symboles, mais je ne peux pas obtenir ma notation de préfixe pour fonctionner (infix, d'autre part, fonctionne). Je suppose que c'est un problème de niveau, mais n'a pas pu le résoudre. Des idées?

Variable (X R: Type)(x:X)(r:R). 
Variable In: X -> R -> Prop. 
Variable rt:> R -> Type. 
Variable rTr: forall (x:X)(y:R), In x y -> y. 
Notation "' a b" := (rTr a b I) (at level 9). 
(* Check ' x r. -- Syntax error: [constr:operconstr] expected after 
[constr:operconstr level 200] (in [constr:operconstr]). *) 

Notation "a ' b" := (rTr a b I) (at level 9). 
Fail Check x ' r. (* Works (half-compiles) *) 
Print Grammar constr. 
(* ... 
| "9" LEFTA 
    [ SELF; "'"; NEXT 
    | "'"; constr:operconstr LEVEL "200"; NEXT 
... *) 

Answer 1

L'astuce était de préciser le niveau de a au moins aussi bas que celui de '. En outre, les deux devaient être inférieur à 10:

Notation "' a b" := (rTr a b I) (at level 9, a at level 9). 
Fail Check ' x r. (* Works (half-compiles) *) 

En outre, la version abbreviation de la notation préfixe travaillé avec/les problèmes (le seul inconvénient étant que les symboles, sont interdits dans les abréviations):

Notation T a b := (rTr a b I). 
Fail Check T x r. (* Works (half-compiles) *)