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