matita
BellLabs
Cachan
Dyade
Eindhoven
IdealX
Marseille
Montevideo
Muenchen
Nancy
Paris
Rocq/TreeAutomata
Rocq/tutto tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY
Sophia-Antipolis/Bertrand
Suresnes
Utrecht

++++++++++++++++

contrib di matita?

++++++++++++++++
[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

coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
orsay: nuovo nucleo diverge (vedi sopra)
Sophia-Antipolis/Buchberger: nuovo nucleo diverge

Sophia-Antipolis/huffmann: Unknown constant
Sophia-Antipolis/MATH/GROUPS: Unknown constant

lyon: Appl con meno di due argomenti, cic:/Lyon/COINDUCTIVES/STREAMS/Alter/eqalters_III.con

Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
Sophia-Antipolis/Algebra: vecchio nucleo variabili
lyon.ok: vecchio nucleo, variabili

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

============= BUG VECCHIO NUCLEO =======================
Problema con permutazione ens?
cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con

============= 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))