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
|
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
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
Probleme de Reset Initial.
Load Field.
Reset Initial.
Coq < Load Field.
Error while reading ./Field.v :
File "./Field.v", line 6, characters 0-83
Error: list already exists
(* l'erreur ne se produit pas sur un fichier plus court ..)
voir dans library states.ml
la fonction freeze=set_state qui modifie l'etat initial ....
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])
CONTRIBS
---------
BellLabs/lazyPCF : OK
Bordeaux/TREES :
Bordeaux/Additions :
echecs sur Realizer
Bordeaux/GROUPS : OK
Bordeaux/EXCEPTIONS :
Hints Unfold n'unfold plus les Local => échec d'Auto
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
Rocq/DEMOS/Demo_AutoRewrite
Anomaly: Invalid argument "output_value: functional value".
Montevideo/CtlTctl OK
Montevideo/RailroadCrossing
File "./railroad_crossing.v", line 613, characters 2-20
Anomaly: useInversionLemma. Please report.
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.
|
