1 CONTENUTO alluris.txt.OK:
3 matita tranne freescale e tests
17 Rocq tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY
18 Sophia-Antipolis tranne algebra, buchberger, math_groups, float, geometry
24 [CoRN: calcolo grafi da caricare troppo lento]
25 [Coq: calcolo grafi da caricare troppo lento]
26 [Sophia-Antipolis: calcolo grafi da caricare troppo lento]
28 CoRN: type-checking vecchio nucleo troppo lento
29 Rocq/AILS: type-checking vecchio nucleo troppo lento
30 Rocq/COC: type-checking vecchio nucleo troppo lento
31 nijmegen: type-checking vecchio nucleo troppo lento
32 Sophia-Antipolis/Float: vecchio nucleo troppo lento
33 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
34 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
36 matita/tests: nuovo nucleo problema con universi!!!
38 Sophia-Antipolis/Algebra: nuovo nucleo diverge
39 cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
40 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
41 cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
42 matita/freescale: nuovo nucleo molto piu' lento del vecchio?
44 lannion: nuovo nucleo impredicative set
45 rocq.higman: nuovo nucleo impredicative set
46 lyon.impredicative_set: nuovo nucleo impredicative set
48 ============= IMPREDICATIVE SET ======================
52 Lyon/CoinductiveExamples
54 Rocq/Paradoxes: Hurkens e Russell
55 Rocq/HistoricalExamples
58 ============= CONVERSIONE FIX GENERATIVI ================
59 cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
60 Appl: wrong application of le_S_n: the parameter H1 has type
61 le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
62 but it should have type
63 le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
65 cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
66 Appl: wrong application of ...
67 (eq (prod (list Key) Data) (pair (list Key) Data lk d)
68 (pair (list Key) Data x0 x))
69 (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
70 (eq (prod (list Key) Data) (pair (list Key) Data lk d)
71 (pair (list Key) Data x0 x))
72 (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
74 cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
75 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
76 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
77 (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
78 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
79 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
80 but it should have type
81 In C (B2C (K2B (KeyAB d0 d1)))
82 (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
84 cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
85 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
86 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
87 (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
88 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
89 (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
90 but it should have type
91 In C (B2C (K2B (KeyAB d0 d1)))
92 (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
94 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
95 Branch for constructor xI :=
97 λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
98 has type ∀p0: positive.
100 eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
101 (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
102 not convertible with positive
105 eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
106 (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
108 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
109 has type ∀p0: positive.
111 eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
112 (plus (plus m (Pmult_nat p (plus m m)))
113 (plus m (Pmult_nat p0 (plus m m))))
114 not convertible with positive
117 eq nat (Pmult_nat (Pplus (xI p) p0) n)
118 (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
120 cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
121 has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
122 not convertible with positive
124 eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
127 cic:/Coq/NArith/BinPos/Pplus_comm.con
128 has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
129 not convertible with positive
130 → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
133 cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
134 has type ∀p0: positive.
135 eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
136 not convertible with positive
138 eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
141 cic:/Coq/NArith/BinPos/Pplus_assoc.con
142 eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
143 (xI (Pplus (Pplus_carry x1 y0) z0))
144 not convertible with positive
146 eq positive (Pplus (xI x1) (Pplus (xI y0) p))
147 (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
149 cic:/Coq/NArith/BinPos/Pplus_reg_r.con
150 has type ∀y1: positive.
151 ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
152 eq positive (xI x1) (xI y1)
153 not convertible with positive
155 eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
156 → eq positive (xI x1) p) (xI __1)
158 cic:/Coq/NArith/BinPos/ZL10.con
159 has type ∀q: positive.
160 ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
161 eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
162 not convertible with positive
164 eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
165 → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
166 End: cic:/Coq/NArith/BinPos/ZL10.con
168 cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
169 has type ∀q: positive.
170 ∀H: eq comparison (Pcompare p q Eq) Gt.
173 and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
176 match h return λp0:positive. positive
177 [ xI ⇒ λy':positive. xO (Pplus_carry q y')
178 | xO ⇒ λy':positive. xI (Pplus q y')
179 | xH ⇒ xO (Psucc q)] (xI p))
180 (or (eq positive h xH)
181 (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
182 (IsPos (Ppred h))))))
183 not convertible with positive
185 eq comparison (Pcompare (xI p) p0 Eq) Gt
188 and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
189 (and (eq positive (Pplus p0 h) (xI p))
190 (or (eq positive h xH)
191 (eq positive_mask (Pminus_mask_carry (xI p) p0)
192 (IsPos (Ppred h))))))) (xI __1)
194 cic:/Coq/NArith/BinPos/Pplus_diag.con
196 ∀IHx: eq positive (Pplus x0 x0) (xO x0).
197 eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
198 but it should have type
200 eq positive (Pplus p p) (xO p)
201 → eq positive (Pplus (xI p) (xI p)) (xO (xI p))