Declaration de Local a l'interieur d'un but ...
Certains Clear deviennent impossible car la variable apparait dans 
un lemme local, c'est plutot sain ...

La syntaxe <A>x=y est parfois refusee

l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les
binding je pense) d'ou des erreurs de syntaxe ...  pure_numarg est
plus sûr 
REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la
syntaxe, elle est incompatible avec L_tac.

CONTRIBS
---------
BellLabs/lazyPCF : OK

Bordeaux/TREES :
Bordeaux/Additions :
  echecs sur Realizer

Bordeaux/GROUPS : OK
Bordeaux/EXCEPTIONS : OK

Dyade/Otway-Rees : OK
Dyade/BDD : 
File "./bdd4.v", line 122, characters 10-28
--> Out of memory après plus de 500Mo utilisés

Rocq/MUTUAL-EXCLUSION : échec sur Realizer

Rocq/COC
Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v
File "./Int_typ.v", line 209, characters 30-44
Problème d'alias dépendant dans un Cases (idem SUBST)

Rocq/ALGEBRA/SETOIDS
--> Token "=_S" non reconnus

Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
--> Un Refine mal typé et des Realizer

Rocq/GRAPHS
File "./cgraph.v", line 2628, characters 14-46
Anomaly: Search error. Please report.

Rocq/PARADOXES OK
Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/DEMOS OK
Rocq/HIGMAN OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK
Rocq/THREE_GAP OK
Rocq/ZF OK

Rocq/SUBST
File "./inversionSL.v", line 215, characters 38-39
Problème d'alias dépendant dans un Cases

Rocq/SCHROEDER
File "./Schroeder.v", line 351, characters 4-52
Anomaly: type_of: variable h1 unbound. Please report.
--> Pb de "Remark" local à un thm pas pris en compte dans
l'environnement de la preuve de ce théorème

Rocq/RATIONAL
--> Des fichiers ML à porter

Lyon/AUTOMATA OK
Lyon/CIRCUITS OK
Lyon/COINDUCTIVES OK
Lyon/IEEE754 OK
Lyon/PROCESSES OK
Lyon/PROGRAMS : Nécessite Programs.v
Lyon/STREAMS OK
Lyon/FIRING-SQUAD : des identificateurs avec le symbole $ !! (plus autorisé)
Lyon/INSERTION-SORT : Nécessite Programs.v
Lyon/DISTRIBUTED_REFERENCE_COUNTING -> Preuve incomplète (lié à Intuition)

Marseille/CCS OK
Marseille/CIRCUITS -> Realizer

Montevideo/CtlTctl OK
Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)

Nancy/FOUnify OK

Nijmegen OK

Paris/ZF OK

Sophia-Antipolis/Cours-de-Coq
File "./ps.v", line 206, characters 3-31
Error: A is already used
Sophia-Antipolis/HARDWARE ??
Sophia-Antipolis/MATHS ??
Sophia-Antipolis/condom ... vide 
Sophia-Antipolis/param_pi
File "./fresh.v", line 173, characters 0-20
Error: Too few occurences

Utrecht/Ramsey OK
Utrecht/ABP OK