Declaration de Local a l'interieur d'un but ...

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

CONTRIBS
---------
BellLabs/lazyPCF/OpSem/
File "./utils.v", line 231, characters 14-18
Syntax error: [Tactic.constrarg_binding_list] expected after [Tactic.numarg] (in [Tactic.simple_tactic])
Specialize A2 with ...

Bordeaux/TREES :
File "./ABR.v", line 131, characters 0-88
Anomaly: Unrecognizable ast node of vernac arg:
 (COMMAND (PROP {Null})). Please report.

Derive Inversion_clear HAS_INV with 
    (n,p:nat)(t1,t2:bintree)(has (bin n t1 t2) p).

Bordeaux/Additions : 
	echecs sur Realizer

Bordeaux/GROUPS : OK

Rocq/GRAPHS
File "./lsort.v", line 82, characters 4-17
Error: Impossible to unify ad with
 (a:ad)(?334 a)->(?334 (ad_double_plus_un a))
Induction a.

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/RATIONAL
	Rewrite/LeibnizRewrite
/home/cpaulin/coq/V7/bin/coqc  -q -byte -I . -I ../MLstuff HS
[Loading ML file struct.cmo ...done]
[Loading ML file sort_tac.cmo ...failed]
File "./HS.v", line 6, characters 0-30
Error: Cannot link ml-object sort_tac.cmo to Coq code.

Rocq/SUBST
File "./TS.v", line 69, characters 0-6
Error: Attempt to save an incomplete proof

Montevideo/CtlTctl OK
Montevideo/RailroadCrossing
File "./railroad_crossing.v", line 613, characters 2-20
Anomaly: useInversionLemma. Please report.