]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/TEST
Working and broken URIs.
[helm.git] / helm / software / components / ng_kernel / TEST
1 BellLabs
2 Cachan
3 Dyade
4 Eindhoven
5 IdealX
6 Montevideo
7 Nancy
8 Paris
9 Utrecht
10
11 ++++++++++++++++
12 CoRN: calcolo grafi da caricare troppo lento
13 Coq: calcolo grafi da caricare troppo lento
14 Sophia-Antipolis: calcolo grafi da caricare troppo lento
15
16 Suresnes: nuovo nucleo
17
18 Rocq/AILS: type-checking vecchio nucleo troppo lento
19 Rocq/COC: type-checking vecchio nucleo troppo lento
20 nijmegen: type-checking vecchio nucleo troppo lento
21 Rocq/TreeAutomata vecchio nucleo troppo lento
22 orsay: type-checking vecchio nucleo troppo lento
23
24 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
25
26 Altre Rocq: bug vari nuovo nucleo, compresi universi!
27 matita: nuovo nucleo universi e altro
28 lyon.ok: vecchio nucleo, variabili
29 marseille: vecchio nucleo, guarded by constructors
30 muenchen: nuovo nucleo, guarded by
31 cachan: nuovo nucleo, guarded by cic:/Coq/Init/Wf/Acc_ind.con
32
33 lannion: nuovo nucleo impredicative set
34 lyon.impredicative_set: nuovo nucleo impredicative set. Altro?
35
36 ============= IMPREDICATIVE SET ======================
37 Lannion/Continuations
38 Lyon/GraphBasics
39 Lyon/Multiplier
40 Lyon/CoinductiveExamples
41 Lyon/Streams
42 Rocq/Paradoxes: Hurkens e Russell
43 Rocq/HistoricalExamples
44 Rocq/HigmanNW
45
46 ============= BUG VECCHIO NUCLEO =======================
47 Problema con permutazione ens?
48 cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
49
50 ============= CONVERSIONE FIX GENERATIVI ================
51 cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
52 Appl: wrong application of le_S_n: the parameter H1 has type
53 le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
54 but it should have type
55 le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
56
57 cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
58 Appl: wrong application of ...
59   (eq (prod (list Key) Data) (pair (list Key) Data lk d)
60     (pair (list Key) Data x0 x))
61   (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
62   (eq (prod (list Key) Data) (pair (list Key) Data lk d)
63     (pair (list Key) Data x0 x))
64   (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
65
66 cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
67 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
68   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
69   (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
70 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
71   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
72 but it should have type
73 In C (B2C (K2B (KeyAB d0 d1)))
74   (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
75
76 cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
77 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
78   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
79   (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
80 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
81   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
82 but it should have type
83 In C (B2C (K2B (KeyAB d0 d1)))
84   (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
85
86 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
87 Branch for constructor xI :=
88 λp0:positive.
89  λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
90 has type ∀p0: positive.
91  ∀n: nat.
92   eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
93     (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
94 not convertible with positive
95  → (λp0:positive.
96        ∀n: nat.
97         eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
98           (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
99
100 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
101 has type ∀p0: positive.
102  ∀m: nat.
103   eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
104     (plus (plus m (Pmult_nat p (plus m m)))
105       (plus m (Pmult_nat p0 (plus m m))))
106 not convertible with positive
107  → (λp0:positive.
108        ∀n: nat.
109         eq nat (Pmult_nat (Pplus (xI p) p0) n)
110           (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
111
112 cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
113 has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
114 not convertible with positive
115  → (λp0:positive.
116        eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
117        (xI __1)
118
119 cic:/Coq/NArith/BinPos/Pplus_comm.con
120 has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
121 not convertible with positive
122  → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
123        (xI __1)
124
125 cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
126 has type ∀p0: positive.
127  eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
128 not convertible with positive
129  → (λp0:positive.
130        eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
131        (xI __1)
132
133 cic:/Coq/NArith/BinPos/Pplus_assoc.con
134  eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
135    (xI (Pplus (Pplus_carry x1 y0) z0))
136 not convertible with positive
137  → (λp:positive.
138        eq positive (Pplus (xI x1) (Pplus (xI y0) p))
139          (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
140
141 cic:/Coq/NArith/BinPos/Pplus_reg_r.con
142 has type ∀y1: positive.
143  ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
144   eq positive (xI x1) (xI y1)
145 not convertible with positive
146  → (λp:positive.
147        eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
148         → eq positive (xI x1) p) (xI __1)
149
150 cic:/Coq/NArith/BinPos/ZL10.con
151 has type ∀q: positive.
152  ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
153   eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
154 not convertible with positive
155  → (λp0:positive.
156        eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
157         → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
158       End: cic:/Coq/NArith/BinPos/ZL10.con
159
160 cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
161 has type ∀q: positive.
162  ∀H: eq comparison (Pcompare p q Eq) Gt.
163   ex positive
164     (λh:positive.
165       and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
166         (and
167           (eq positive
168             match h return λp0:positive. positive
169              [ xI ⇒ λy':positive. xO (Pplus_carry q y')
170              | xO ⇒ λy':positive. xI (Pplus q y')
171              | xH ⇒ xO (Psucc q)]  (xI p))
172           (or (eq positive h xH)
173             (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
174               (IsPos (Ppred h))))))
175 not convertible with positive
176  → (λp0:positive.
177        eq comparison (Pcompare (xI p) p0 Eq) Gt
178         → ex positive
179               (λh:positive.
180                 and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
181                   (and (eq positive (Pplus p0 h) (xI p))
182                     (or (eq positive h xH)
183                       (eq positive_mask (Pminus_mask_carry (xI p) p0)
184                         (IsPos (Ppred h))))))) (xI __1)
185
186 cic:/Coq/NArith/BinPos/Pplus_diag.con
187 ∀x0: positive.
188  ∀IHx: eq positive (Pplus x0 x0) (xO x0).
189   eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
190 but it should have type
191 ∀p: positive.
192  eq positive (Pplus p p) (xO p)
193   → eq positive (Pplus (xI p) (xI p)) (xO (xI p))
194
195