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
Error: Tactic generated a subgoal identical to the original goal.


Lyon/AUTOMATA : OK
Lyon/CIRCUITS : OK
Lyon/COINDUCTIVES : 
File "./Examples.v", line 276, characters 0-764
Error: Incorrect elimination of H in the inductive type
 eq
The elimination predicate
 [a1:A; _:((hd (Cons s0 H))=(hd (Cons s a0))); a2:A]
  (EqSt2 A (Cons s0 H) (Cons a2 a0)) has type
 A->(hd (Cons s0 H))=(hd (Cons s a0))->A->Prop
It should be one of :
 (a:A)(hd (Cons a0 s0))=a->Prop, (a:A)(hd (Cons a0 s0))=a->Set,
 A->Prop, A->Set
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

Lyon/IEEE754 : OK

Rocq/DEMOS : OK
Rocq/GRAPHS
/home/cpaulin/TYPES/V7/bin/coqc  -q  -I . lsort
Utilise NewInduction

/home/cpaulin/TYPES/V7/bin/coqc  -q  -I . cgraph
Warning: Found several default clauses, kept the first one

File "./cgraph.v", line 1866, characters 2-7
Error: frontier was handed back a ill-formed proof.
(Apres un EApply)

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
Error: In environment
int_typ : term->intP->(s:skel)(Can s)
T  : term
ip  : intP
s  : skel
A  : term
B  : term
_  : skel
_  : skel
s1  := s : skel
The term (default_can s1) has type (Can s1)
 while it is expected to have type (Can (PROD _ s1))

Rocq/ALGEBRA/RELATIONS/Relations.v
--> Un problème de Coercion au discharge

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

Rocq/PARADOXES
File "./Reynolds1.v", line 105, characters 0-429
Error: checking of theorem per_F0 failed... aborting

Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/DEMOS OK
Rocq/HIGMAN OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK

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/SUBST
File "./TS.v", line 69, characters 0-6
Error: Attempt to save an incomplete proof

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

Nijmegen OK
Utrecht/Ramsey OK

Utrecht/ABP
coqc  -q  -I . abp_base
File "./abp_base.v", line 42, characters 0-154
Error: Cannot declare a variable or hypothesis over the term Y
because this term is not a type.