1 CONTENUTO alluris.txt.OK:
15 Rocq tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY
16 Sophia-Antipolis tranne algebra, buchberger, huffmann, math_groups,
27 [CoRN: calcolo grafi da caricare troppo lento]
28 [Coq: calcolo grafi da caricare troppo lento]
29 [Sophia-Antipolis: calcolo grafi da caricare troppo lento]
31 CoRN: type-checking vecchio nucleo troppo lento
32 Rocq/AILS: type-checking vecchio nucleo troppo lento
33 Rocq/COC: type-checking vecchio nucleo troppo lento
34 nijmegen: type-checking vecchio nucleo troppo lento
35 Sophia-Antipolis/Float: vecchio nucleo troppo lento
36 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
38 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
39 orsay: nuovo nucleo diverge (vedi sopra)
40 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
42 Sophia-Antipolis/huffmann: Unknown constant
43 Sophia-Antipolis/MATH/GROUPS: Unknown constant
45 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo: ???
46 Sophia-Antipolis/Algebra: vecchio nucleo variabili
47 lyon/PROCESSES: vecchio nucleo, variabili
49 lannion: nuovo nucleo impredicative set
50 rocq.higman: nuovo nucleo impredicative set
51 lyon.impredicative_set: nuovo nucleo impredicative set
53 ============= IMPREDICATIVE SET ======================
57 Lyon/CoinductiveExamples
59 Rocq/Paradoxes: Hurkens e Russell
60 Rocq/HistoricalExamples
63 ============= BUG VECCHIO NUCLEO =======================
64 Problema con permutazione ens?
65 cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
67 ============= CONVERSIONE FIX GENERATIVI ================
68 cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
69 Appl: wrong application of le_S_n: the parameter H1 has type
70 le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
71 but it should have type
72 le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
74 cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
75 Appl: wrong application of ...
76 (eq (prod (list Key) Data) (pair (list Key) Data lk d)
77 (pair (list Key) Data x0 x))
78 (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
79 (eq (prod (list Key) Data) (pair (list Key) Data lk d)
80 (pair (list Key) Data x0 x))
81 (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
83 cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
84 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
85 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
86 (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
87 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
88 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
89 but it should have type
90 In C (B2C (K2B (KeyAB d0 d1)))
91 (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
93 cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
94 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
95 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
96 (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
97 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
98 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
99 but it should have type
100 In C (B2C (K2B (KeyAB d0 d1)))
101 (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
103 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
104 Branch for constructor xI :=
106 λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
107 has type ∀p0: positive.
109 eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
110 (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
111 not convertible with positive
114 eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
115 (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
117 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
118 has type ∀p0: positive.
120 eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
121 (plus (plus m (Pmult_nat p (plus m m)))
122 (plus m (Pmult_nat p0 (plus m m))))
123 not convertible with positive
126 eq nat (Pmult_nat (Pplus (xI p) p0) n)
127 (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
129 cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
130 has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
131 not convertible with positive
133 eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
136 cic:/Coq/NArith/BinPos/Pplus_comm.con
137 has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
138 not convertible with positive
139 → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
142 cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
143 has type ∀p0: positive.
144 eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
145 not convertible with positive
147 eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
150 cic:/Coq/NArith/BinPos/Pplus_assoc.con
151 eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
152 (xI (Pplus (Pplus_carry x1 y0) z0))
153 not convertible with positive
155 eq positive (Pplus (xI x1) (Pplus (xI y0) p))
156 (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
158 cic:/Coq/NArith/BinPos/Pplus_reg_r.con
159 has type ∀y1: positive.
160 ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
161 eq positive (xI x1) (xI y1)
162 not convertible with positive
164 eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
165 → eq positive (xI x1) p) (xI __1)
167 cic:/Coq/NArith/BinPos/ZL10.con
168 has type ∀q: positive.
169 ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
170 eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
171 not convertible with positive
173 eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
174 → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
175 End: cic:/Coq/NArith/BinPos/ZL10.con
177 cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
178 has type ∀q: positive.
179 ∀H: eq comparison (Pcompare p q Eq) Gt.
182 and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
185 match h return λp0:positive. positive
186 [ xI ⇒ λy':positive. xO (Pplus_carry q y')
187 | xO ⇒ λy':positive. xI (Pplus q y')
188 | xH ⇒ xO (Psucc q)] (xI p))
189 (or (eq positive h xH)
190 (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
191 (IsPos (Ppred h))))))
192 not convertible with positive
194 eq comparison (Pcompare (xI p) p0 Eq) Gt
197 and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
198 (and (eq positive (Pplus p0 h) (xI p))
199 (or (eq positive h xH)
200 (eq positive_mask (Pminus_mask_carry (xI p) p0)
201 (IsPos (Ppred h))))))) (xI __1)
203 cic:/Coq/NArith/BinPos/Pplus_diag.con
205 ∀IHx: eq positive (Pplus x0 x0) (xO x0).
206 eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
207 but it should have type
209 eq positive (Pplus p p) (xO p)
210 → eq positive (Pplus (xI p) (xI p)) (xO (xI p))