Coq: Fixation d'une notation récursive

Question

Voici une notation récursive simple, demi-travail:

Universe ARG. Definition ARG := Type@{ARG}. 
Parameter X: ARG. 
Notation A := (fun x:ARG->ARG => fun y:x X => y). 
Parameter P: ARG -> ARG. 
Parameter s: P X. 
Notation "[ x .. z u ]" := (x P .. (z P u) ..) (at level 5, z, u at next level). 
Check (A P (A P (A P s))). (* [A A A s]: P X *) 
Print Grammar constr. 
(*| "5" RIGHTA 
    [ "["; NEXT; LIST1 NEXT; NEXT; "]" 
    | "["; NEXT; NEXT; "]" ]*) 
Check [A A A s]. (* Syntax error: [constr:operconstr] or [constr:operconstr] expected (in [constr:operconstr]). *) 

Comme vous le voyez, Coq reconnaît A P (A P (A P s)) comme [A A A s]: P X mais ne peut pas analyser [A A A s]. Où est le problème, quelle est la solution?

EDIT: Coq semble avoir besoin de quelques "outils d'analyse" ici. Par exemple, les travaux suivants:

Notation "(x .. z [ u ])" := (x P .. (z P u) ..) (at level 5, z at next level). 
Check (A A A [s]): P X. 

Comme je voudrais me débarrasser de la notation interne, la question reste ouverte

Answer 1

Le problème est que Coq < = 8,7 ne supporte pas les notations récursives de la Formulaire x .. y z très bien, et la solution est de télécharger le maître Coq, ou attendre Coq 8.8. Hugo Herbelin's fix, entitled Adding support for recursive notations of the form "x , .. , y , z", a été fusionné le 1 août 2017.