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
|
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.
|
