AddPath "/toto".
Anomaly: Uncaught exception Unix.Unix_error(20, "stat", "/toto").
Please report.


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

Les arguments des Tactic Definition sont interpretes avant 
l'application de la tactique, ils ne peuvent pas contenir des variables 
qui seront introduites dans la tactique ....
MUTUAL-EXCLUSION/binary/version1/Soundness.v

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.

Associativite Repeat Orelse changee
	Repeat A Orelse B se lit (Repeat A) Orelse B 
ce n'est pas malin car Repeat A n'echoue jamais

les parentheses ne sont pas autorises autour de 
motifs constants :
> Check [n:nat]Cases n of (O) => true | _ => false end.
Syntax error: 'as' or ',' or [ne_pattern_list] expected after
[Constr.pattern] (in [compound_pattern])        ...CORRIGE

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

Bordeaux/TREES :
Bordeaux/Additions : 
	echecs sur Realizer

Bordeaux/GROUPS : OK

Bordeaux/EXCEPTIONS : OK

Dyade/Otway-Rees : OK
Dyade/BDD : Require Rocq/GRAPHS

Lyon/AUTOMATA : OK
Lyon/IEEE754 : OK
Lyon/COINDUCTIVES : OK

Rocq/GRAPHS
/home/cpaulin/TYPES/V7/bin/coqc  -q  -I . lsort
Warning: compute_metamap: MV(1506) sans type !
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/
	Incompatibilite interpretation des arguments de Tactic Definition

Rocq/COC
File "./Conv_Dec.v", line 68, characters 2-459
Error: Inference of annotation not yet implemented in this case

Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
Anomaly: Search error. Please report.
Refine 

Rocq/PARADOXES
File "./BuraliForti.v", line 176, characters 0-26
Anomaly: Uncaught exception Univ.UniverseInconsistency. Please report.
A la fermeture de section, est-ce normal ? pourquoi une anomalie ?

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

Rocq/SCHROEDER
File "./Functions.v", line 95, characters 0-15
Error: Bad inductive definition.
A la fermeture de section

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.