======================================================================
Conventions lexicales
======================================================================

 INFIX = suites de symboles speciaux, repartis en plusieurs
         categories correspondant a des precedences differentes
         (comme en ocaml)

 si `s' est un infix, alors `@s' est un IDENT correspondant au
 symbole (prefixe) correspondant

 d'ou    definition $+ := plus;
         check O + O;

======================================================================
Constr
======================================================================

simple_constr 
  ::= qident
    | "\" binders "." constr       \\ lambda
    | "!" binders "." constr       \\ produit
    | constr "->" constr           \\ assoc droite
    | "(" simple_constr+ ")"
    | "cases" constr "of" OPT "|" LIST0 equation SEP "|" "end"
    | "fix" ident "where" LIST1 recursive SEP "and"
    | "Set"
    | "Prop"
    | "Type"
    | "?"
    | constr infix constr          \\ =, +, -, *, /, **, ++, etc.
                                   \\ /\ and ? \/ or ?
    | "~" constr                   \\ not ?

constr 
  ::= simple_constr+

binders
  ::= LIST1 ident SEP ","
    | LIST1 binder SEP ","

binder
  ::= LIST1 ident SEP "," ":" constr

equation
  ::= pattern "=>" constr

pattern
  ::= 

recursive
  ::= ident binders "{" "struct" ident "}" ":" constr ":=" constr


======================================================================
Tactic
======================================================================


======================================================================
Vernac
======================================================================

vernac 
  ::= "definition" ...
    | "fixpoint" LIST1 recursive SEP "and"