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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
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.
|
