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
|
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 "./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/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/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/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
Rocq/MM
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.
--> Pb de calcul de de Bruijn dans le vieux Match
|
