blob: d29d146d98da1a5f4e0df9a507bf63dc11454297 (
plain)
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
|
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
|
