--- /dev/null
+CONTENUTO alluris.txt.OK, NEW typing, OLD typing
+
+matita 11.89 11.71 tranne freescale
+Coq fixpoints
+BellLabs 0.21 0.22
+Cachan .....
+Dyade fixpoints
+Eindhoven 0.23 0.85
+IdealX 0.05 0.06
+Lyon impredicative set
+Marseille 1.04 2.23
+Montevideo 1.90 4.29
+Muenchen 0.05 0.07
+Nancy 0.13 0.24
+Orsay fixpoints
+Paris 0.39 0.48
+Rocq impredicative set tranne ails, coc, higman,
+ ALGEBRA/CATEGORY_THEORY
+Sophia-Antipolis tranne algebra, buchberger,
+ math_groups, float, geometry
+Suresnes fixpoints
+Utrecht 0.82 0.92
+
+++++++++++++++++
+
+TODO: Andrea mi ha cassato la parte sulla reentrance; secondo me quella e'
+importante
+
+ATTENZIONE: cosa succede con un PTS non full? Un (Prod : Type) non lo tipiamo,
+ma tipiamo (Lambda : Type)!
+
+file bug_universi.ma: sbaglia a fare il ranking!
+
+[CoRN: calcolo grafi da caricare troppo lento]
+[Coq: calcolo grafi da caricare troppo lento]
+[Sophia-Antipolis: calcolo grafi da caricare troppo lento]
+
+CoRN: type-checking vecchio nucleo troppo lento
+Rocq/AILS: type-checking vecchio nucleo troppo lento
+Rocq/COC: type-checking vecchio nucleo troppo lento
+nijmegen: type-checking vecchio nucleo troppo lento
+Sophia-Antipolis/Float: vecchio nucleo troppo lento
+Sophia-Antipolis/geometry: vecchio nucleo troppo lento
+Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
+
+## = diventato addirittura velocissimo dopo universi + proof irrelevance + altezze
+##Sophia-Antipolis/Algebra: nuovo nucleo diverge
+## cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
+##Sophia-Antipolis/Buchberger: nuovo nucleo diverge
+## cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
+matita/freescale: nuovo nucleo molto piu' lento del vecchio?
+
+lannion: nuovo nucleo impredicative set
+rocq.higman: nuovo nucleo impredicative set
+lyon.impredicative_set: nuovo nucleo impredicative set
+
+============= IMPREDICATIVE SET ======================
+Lannion/Continuations
+Lyon/GraphBasics
+Lyon/Multiplier
+Lyon/CoinductiveExamples
+Lyon/Streams
+Rocq/Paradoxes: Hurkens e Russell
+Rocq/HistoricalExamples
+Rocq/HigmanNW
+
+============= CONVERSIONE FIX GENERATIVI ================
+cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
+Appl: wrong application of le_S_n: the parameter H1 has type
+le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
+but it should have type
+le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
+
+cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
+Appl: wrong application of ...
+ (eq (prod (list Key) Data) (pair (list Key) Data lk d)
+ (pair (list Key) Data x0 x))
+ (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
+ (eq (prod (list Key) Data) (pair (list Key) Data lk d)
+ (pair (list Key) Data x0 x))
+ (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
+
+cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
+Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
+ (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
+ (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
+or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
+ (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
+but it should have type
+In C (B2C (K2B (KeyAB d0 d1)))
+ (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
+
+cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
+Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
+ (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
+ (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
+or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
+ (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
+but it should have type
+In C (B2C (K2B (KeyAB d0 d1)))
+ (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
+
+cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
+Branch for constructor xI :=
+λp0:positive.
+ λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
+has type ∀p0: positive.
+ ∀n: nat.
+ eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
+ (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
+not convertible with positive
+ → (λp0:positive.
+ ∀n: nat.
+ eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
+ (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
+
+cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
+has type ∀p0: positive.
+ ∀m: nat.
+ eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
+ (plus (plus m (Pmult_nat p (plus m m)))
+ (plus m (Pmult_nat p0 (plus m m))))
+not convertible with positive
+ → (λp0:positive.
+ ∀n: nat.
+ eq nat (Pmult_nat (Pplus (xI p) p0) n)
+ (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
+
+cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
+has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
+not convertible with positive
+ → (λp0:positive.
+ eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
+ (xI __1)
+
+cic:/Coq/NArith/BinPos/Pplus_comm.con
+has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
+not convertible with positive
+ → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
+ (xI __1)
+
+cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
+has type ∀p0: positive.
+ eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
+not convertible with positive
+ → (λp0:positive.
+ eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
+ (xI __1)
+
+cic:/Coq/NArith/BinPos/Pplus_assoc.con
+ eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
+ (xI (Pplus (Pplus_carry x1 y0) z0))
+not convertible with positive
+ → (λp:positive.
+ eq positive (Pplus (xI x1) (Pplus (xI y0) p))
+ (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
+
+cic:/Coq/NArith/BinPos/Pplus_reg_r.con
+has type ∀y1: positive.
+ ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
+ eq positive (xI x1) (xI y1)
+not convertible with positive
+ → (λp:positive.
+ eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
+ → eq positive (xI x1) p) (xI __1)
+
+cic:/Coq/NArith/BinPos/ZL10.con
+has type ∀q: positive.
+ ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
+ eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
+not convertible with positive
+ → (λp0:positive.
+ eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
+ → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
+ End: cic:/Coq/NArith/BinPos/ZL10.con
+
+cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
+has type ∀q: positive.
+ ∀H: eq comparison (Pcompare p q Eq) Gt.
+ ex positive
+ (λh:positive.
+ and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
+ (and
+ (eq positive
+ match h return λp0:positive. positive
+ [ xI ⇒ λy':positive. xO (Pplus_carry q y')
+ | xO ⇒ λy':positive. xI (Pplus q y')
+ | xH ⇒ xO (Psucc q)] (xI p))
+ (or (eq positive h xH)
+ (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
+ (IsPos (Ppred h))))))
+not convertible with positive
+ → (λp0:positive.
+ eq comparison (Pcompare (xI p) p0 Eq) Gt
+ → ex positive
+ (λh:positive.
+ and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
+ (and (eq positive (Pplus p0 h) (xI p))
+ (or (eq positive h xH)
+ (eq positive_mask (Pminus_mask_carry (xI p) p0)
+ (IsPos (Ppred h))))))) (xI __1)
+
+cic:/Coq/NArith/BinPos/Pplus_diag.con
+∀x0: positive.
+ ∀IHx: eq positive (Pplus x0 x0) (xO x0).
+ eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
+but it should have type
+∀p: positive.
+ eq positive (Pplus p p) (xO p)
+ → eq positive (Pplus (xI p) (xI p)) (xO (xI p))
projects / helm.git / blobdiff