helm/software/components/ng_kernel/TEST

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