13 Rocq/tutto tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY
14 Sophia-Antipolis/Bertrand
23 [CoRN: calcolo grafi da caricare troppo lento]
24 [Coq: calcolo grafi da caricare troppo lento]
25 [Sophia-Antipolis: calcolo grafi da caricare troppo lento]
27 CoRN: type-checking vecchio nucleo troppo lento
28 Rocq/AILS: type-checking vecchio nucleo troppo lento
29 Rocq/COC: type-checking vecchio nucleo troppo lento
30 nijmegen: type-checking vecchio nucleo troppo lento
31 Sophia-Antipolis/Float: vecchio nucleo troppo lento
32 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
34 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
35 orsay: nuovo nucleo diverge (vedi sopra)
36 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
38 Sophia-Antipolis/huffmann: Unknown constant
39 Sophia-Antipolis/MATH/GROUPS: Unknown constant
41 lyon: Appl con meno di due argomenti, cic:/Lyon/COINDUCTIVES/STREAMS/Alter/eqalters_body.con
43 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
44 Sophia-Antipolis/Algebra: vecchio nucleo variabili
45 lyon.ok: vecchio nucleo, variabili
47 lannion: nuovo nucleo impredicative set
48 rocq.higman: nuovo nucleo impredicative set
49 lyon.impredicative_set: nuovo nucleo impredicative set
51 ============= IMPREDICATIVE SET ======================
55 Lyon/CoinductiveExamples
57 Rocq/Paradoxes: Hurkens e Russell
58 Rocq/HistoricalExamples
61 ============= BUG VECCHIO NUCLEO =======================
62 Problema con permutazione ens?
63 cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
65 ============= CONVERSIONE FIX GENERATIVI ================
66 cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
67 Appl: wrong application of le_S_n: the parameter H1 has type
68 le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
69 but it should have type
70 le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
72 cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
73 Appl: wrong application of ...
74 (eq (prod (list Key) Data) (pair (list Key) Data lk d)
75 (pair (list Key) Data x0 x))
76 (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
77 (eq (prod (list Key) Data) (pair (list Key) Data lk d)
78 (pair (list Key) Data x0 x))
79 (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
81 cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
82 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
83 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
84 (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
85 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
86 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
87 but it should have type
88 In C (B2C (K2B (KeyAB d0 d1)))
89 (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
91 cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
92 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
93 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
94 (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
95 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
96 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
97 but it should have type
98 In C (B2C (K2B (KeyAB d0 d1)))
99 (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
101 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
102 Branch for constructor xI :=
104 λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
105 has type ∀p0: positive.
107 eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
108 (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
109 not convertible with positive
112 eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
113 (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
115 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
116 has type ∀p0: positive.
118 eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
119 (plus (plus m (Pmult_nat p (plus m m)))
120 (plus m (Pmult_nat p0 (plus m m))))
121 not convertible with positive
124 eq nat (Pmult_nat (Pplus (xI p) p0) n)
125 (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
127 cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
128 has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
129 not convertible with positive
131 eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
134 cic:/Coq/NArith/BinPos/Pplus_comm.con
135 has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
136 not convertible with positive
137 → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
140 cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
141 has type ∀p0: positive.
142 eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
143 not convertible with positive
145 eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
148 cic:/Coq/NArith/BinPos/Pplus_assoc.con
149 eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
150 (xI (Pplus (Pplus_carry x1 y0) z0))
151 not convertible with positive
153 eq positive (Pplus (xI x1) (Pplus (xI y0) p))
154 (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
156 cic:/Coq/NArith/BinPos/Pplus_reg_r.con
157 has type ∀y1: positive.
158 ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
159 eq positive (xI x1) (xI y1)
160 not convertible with positive
162 eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
163 → eq positive (xI x1) p) (xI __1)
165 cic:/Coq/NArith/BinPos/ZL10.con
166 has type ∀q: positive.
167 ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
168 eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
169 not convertible with positive
171 eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
172 → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
173 End: cic:/Coq/NArith/BinPos/ZL10.con
175 cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
176 has type ∀q: positive.
177 ∀H: eq comparison (Pcompare p q Eq) Gt.
180 and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
183 match h return λp0:positive. positive
184 [ xI ⇒ λy':positive. xO (Pplus_carry q y')
185 | xO ⇒ λy':positive. xI (Pplus q y')
186 | xH ⇒ xO (Psucc q)] (xI p))
187 (or (eq positive h xH)
188 (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
189 (IsPos (Ppred h))))))
190 not convertible with positive
192 eq comparison (Pcompare (xI p) p0 Eq) Gt
195 and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
196 (and (eq positive (Pplus p0 h) (xI p))
197 (or (eq positive h xH)
198 (eq positive_mask (Pminus_mask_carry (xI p) p0)
199 (IsPos (Ppred h))))))) (xI __1)
201 cic:/Coq/NArith/BinPos/Pplus_diag.con
203 ∀IHx: eq positive (Pplus x0 x0) (xO x0).
204 eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
205 but it should have type
207 eq positive (Pplus p p) (xO p)
208 → eq positive (Pplus (xI p) (xI p)) (xO (xI p))