Hints Resolve fait une anomalie si la constante n'existe pas

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 : echec sur Realizer
Bordeaux/Additions : echec sur Realizer
Bordeaux/SearchTrees : echec sur Realizer

Bordeaux/GROUPS : OK
Bordeaux/EXCEPTIONS : OK

Dyade/Otway-Rees : OK
Dyade/BDD : 
File "./bdd4.v", line 122, characters 10-28
<<<<<<< PROBLEMES
Error: Tactic generated a subgoal identical to the original goal.

Lyon/AUTOMATA : OK
Lyon/CIRCUITS : OK
Lyon/COINDUCTIVES : 
File "./Specified_Streams.v", line 11, characters 0-132
Error: Illegal application (Type Error): 
The term SStream of type (A:Set)(nat->A->Prop)->Set
cannot be applied to the terms
 A : Set
 x : (SStream A P)
The 2nd term has type (SStream A P) which should be coercible to
 nat->A->Prop

--> Out of memory après plus de 500Mo utilisés

Lyon/IEEE754 : OK
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/TreeAutomata
File "./defs.v", line 309, characters 34-47
Error: Not a recursive eliminator: some induction hypothesis is lacking
--> Bug NewInduction...

File "./lattice_fixpoint.v", line 29, characters 44-57
--> Problème de lookup_eliminator (effet de bord sur le schéma d'élimination)

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
File "./fifo.v", line 181, characters 0-6
Error: Attempt to save an incomplete proof
--> Preuve incomplète (lié à Intuition)

Rocq/MM

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/HARDWARE OK
Sophia-Antipolis/Cours-de-Coq OK

Sophia-Antipolis/MATHS/GEOMETRY
File "./part3.v", line 78, characters 0-5
Error: Attempt to save an incomplete proof
--> Changement de sémantique de Intuition

Sophia-Antipolis/condom ... vide 

Sophia-Antipolis/param_pi
File "./fresh.v", line 173, characters 0-20
Error: Too few occurences

Suresnes/BDD OK

Utrecht/Ramsey OK
Utrecht/ABP OK