1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
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
|
