From c48c7e28f54e00e12755f703a8c46187be701ed2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 11:26:54 +0000 Subject: [PATCH] added a list of uris to ease debugging --- .../software/components/ng_kernel/alluris.txt | 579 ++++++++++++++++++ helm/software/components/ng_kernel/check.ml | 39 +- 2 files changed, 609 insertions(+), 9 deletions(-) create mode 100644 helm/software/components/ng_kernel/alluris.txt diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt new file mode 100644 index 000000000..5c8668c83 --- /dev/null +++ b/helm/software/components/ng_kernel/alluris.txt @@ -0,0 +1,579 @@ +cic:/matita/nat/compare/not_eq_to_eqb_false.con +cic:/matita/nat/compare/nat_compare_to_Prop.con +cic:/matita/nat/compare/nat_compare_pred_pred.con +cic:/matita/nat/compare/nat_compare_n_n.con +cic:/matita/nat/compare/nat_compare_n_m_m_n.con +cic:/matita/nat/compare/nat_compare_elim.con +cic:/matita/nat/compare/nat_compare_S_S.con +cic:/matita/nat/compare/nat_compare.con +cic:/matita/nat/compare/ltb_to_Prop.con +cic:/matita/nat/compare/ltb_elim.con +cic:/matita/nat/compare/ltb.con +cic:/matita/nat/compare/lt_to_leb_false.con +cic:/matita/nat/compare/leb_true_to_le.con +cic:/matita/nat/compare/leb_to_Prop.con +cic:/matita/nat/compare/leb_false_to_not_le.con +cic:/matita/nat/compare/leb_elim.con +cic:/matita/nat/compare/leb_demod3.con +cic:/matita/nat/compare/leb_demod2.con +cic:/matita/nat/compare/leb_demod1.con +cic:/matita/nat/compare/leb.con +cic:/matita/nat/compare/le_to_leb_true.con +cic:/matita/nat/compare/eqb_true_to_eq.con +cic:/matita/nat/compare/eqb_to_Prop.con +cic:/matita/nat/compare/eqb_n_n.con +cic:/matita/nat/compare/eqb_false_to_not_eq.con +cic:/matita/nat/compare/eqb_elim.con +cic:/matita/nat/compare/eqb.con +cic:/matita/nat/compare/eq_to_eqb_true.con +cic:/matita/nat/compare/compare_demod2.con +cic:/matita/nat/compare/compare_demod1.con +cic:/matita/nat/nat/pred_demod2.con +cic:/matita/nat/nat/pred_demod1.con +cic:/matita/nat/nat/pred_Sn.con +cic:/matita/nat/nat/pred.con +cic:/matita/nat/nat/not_zero.con +cic:/matita/nat/nat/not_eq_n_Sn.con +cic:/matita/nat/nat/not_eq_S.con +cic:/matita/nat/nat/not_eq_O_S.con +cic:/matita/nat/nat/nat_rect.con +cic:/matita/nat/nat/nat_rec.con +cic:/matita/nat/nat/nat_ind.con +cic:/matita/nat/nat/nat_elim2.con +cic:/matita/nat/nat/nat_case1.con +cic:/matita/nat/nat/nat_case.con +cic:/matita/nat/nat/nat.ind +cic:/matita/nat/nat/injective_S.con +cic:/matita/nat/nat/inj_S.con +cic:/matita/nat/nat/decidable_eq_nat.con +cic:/matita/nat/orders/transitive_lt.con +cic:/matita/nat/orders/transitive_le.con +cic:/matita/nat/orders/trans_lt.con +cic:/matita/nat/orders/trans_le.con +cic:/matita/nat/orders/not_lt_to_le.con +cic:/matita/nat/orders/not_le_to_lt.con +cic:/matita/nat/orders/not_le_Sn_n.con +cic:/matita/nat/orders/not_le_Sn_O.con +cic:/matita/nat/orders/not_eq_to_le_to_lt.con +cic:/matita/nat/orders/nat_elim1.con +cic:/matita/nat/orders/ltn_to_ltO.con +cic:/matita/nat/orders/lt_to_not_le.con +cic:/matita/nat/orders/lt_to_not_eq.con +cic:/matita/nat/orders/lt_to_lt_S_S.con +cic:/matita/nat/orders/lt_to_le_to_lt.con +cic:/matita/nat/orders/lt_to_le.con +cic:/matita/nat/orders/lt_pred.con +cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con +cic:/matita/nat/orders/lt_S_to_lt.con +cic:/matita/nat/orders/lt_S_to_le.con +cic:/matita/nat/orders/lt_S_S_to_lt.con +cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con +cic:/matita/nat/orders/lt_O_n_elim.con +cic:/matita/nat/orders/lt_O_S.con +cic:/matita/nat/orders/lt.con +cic:/matita/nat/orders/le_to_or_lt_eq.con +cic:/matita/nat/orders/le_to_not_lt.con +cic:/matita/nat/orders/le_to_lt_to_lt.con +cic:/matita/nat/orders/le_to_le_to_eq.con +cic:/matita/nat/orders/le_to_le_pred.con +cic:/matita/nat/orders/le_pred_to_le.con +cic:/matita/nat/orders/le_pred_n.con +cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con +cic:/matita/nat/orders/le_n_fn.con +cic:/matita/nat/orders/le_n_Sn.con +cic:/matita/nat/orders/le_n_Sm_elim.con +cic:/matita/nat/orders/le_n_O_to_eq.con +cic:/matita/nat/orders/le_n_O_elim.con +cic:/matita/nat/orders/le_inv.con +cic:/matita/nat/orders/le_ind.con +cic:/matita/nat/orders/le_S_S_to_le.con +cic:/matita/nat/orders/le_S_S.con +cic:/matita/nat/orders/le_O_n.con +cic:/matita/nat/orders/leS_to_not_zero.con +cic:/matita/nat/orders/le.ind +cic:/matita/nat/orders/increasing_to_monotonic.con +cic:/matita/nat/orders/increasing_to_le2.con +cic:/matita/nat/orders/increasing_to_le.con +cic:/matita/nat/orders/increasing.con +cic:/matita/nat/orders/gt.con +cic:/matita/nat/orders/ge.con +cic:/matita/nat/orders/eq_to_not_lt.con +cic:/matita/nat/orders/decidable_lt.con +cic:/matita/nat/orders/decidable_le.con +cic:/matita/nat/orders/antisymmetric_le.con +cic:/matita/nat/orders/antisym_le.con +cic:/matita/nat/orders/S_pred.con +cic:/matita/nat/orders/Not_lt_n_n.con +cic:/matita/nat/plus/sym_plus.con +cic:/matita/nat/plus/plus_n_Sm.con +cic:/matita/nat/plus/plus_n_SO.con +cic:/matita/nat/plus/plus_n_O.con +cic:/matita/nat/plus/plus_demod4.con +cic:/matita/nat/plus/plus_demod3.con +cic:/matita/nat/plus/plus_demod2.con +cic:/matita/nat/plus/plus_demod1.con +cic:/matita/nat/plus/plus.con +cic:/matita/nat/plus/injective_plus_r.con +cic:/matita/nat/plus/injective_plus_l.con +cic:/matita/nat/plus/inj_plus_r.con +cic:/matita/nat/plus/inj_plus_l.con +cic:/matita/nat/plus/associative_plus.con +cic:/matita/nat/plus/assoc_plus.con +cic:/matita/nat/times/times_n_Sm.con +cic:/matita/nat/times/times_n_SO.con +cic:/matita/nat/times/times_n_O.con +cic:/matita/nat/times/times_demod6.con +cic:/matita/nat/times/times_demod4.con +cic:/matita/nat/times/times_demod2.con +cic:/matita/nat/times/times_demod1.con +cic:/matita/nat/times/times_SSO_n.con +cic:/matita/nat/times/times_SSO.con +cic:/matita/nat/times/times_O_to_O.con +cic:/matita/nat/times/times.con +cic:/matita/nat/times/symmetric_times.con +cic:/matita/nat/times/sym_times.con +cic:/matita/nat/times/or_eq_eq_S.con +cic:/matita/nat/times/distributive_times_plus.con +cic:/matita/nat/times/distr_times_plus.con +cic:/matita/nat/times/associative_times.con +cic:/matita/nat/times/assoc_times.con +cic:/matita/Z/z/pos_n_eq_S_n.con +cic:/matita/Z/z/not_eq_pos_neg.con +cic:/matita/Z/z/not_eq_OZ_pos.con +cic:/matita/Z/z/not_eq_OZ_neg.con +cic:/matita/Z/z/neg_Z_of_nat.con +cic:/matita/Z/z/injective_pos.con +cic:/matita/Z/z/injective_neg.con +cic:/matita/Z/z/inj_pos.con +cic:/matita/Z/z/inj_neg.con +cic:/matita/Z/z/decidable_eq_Z.con +cic:/matita/Z/z/abs.con +cic:/matita/Z/z/Zsucc_Zpred.con +cic:/matita/Z/z/Zsucc.con +cic:/matita/Z/z/Zpred_Zsucc.con +cic:/matita/Z/z/Zpred.con +cic:/matita/Z/z/Z_rect.con +cic:/matita/Z/z/Z_rec.con +cic:/matita/Z/z/Z_of_nat.con +cic:/matita/Z/z/Z_ind.con +cic:/matita/Z/z/Z.ind +cic:/matita/Z/z/OZ_test_to_Prop.con +cic:/matita/Z/z/OZ_test.con +cic:/matita/algebra/monoids/premonoid.con +cic:/matita/algebra/monoids/monoid_properties.con +cic:/matita/algebra/monoids/magma.con +cic:/matita/algebra/monoids/is_semi_group.con +cic:/matita/algebra/monoids/is_right_inverse.con +cic:/matita/algebra/monoids/is_left_inverse_to_is_right_inverse_to_eq.con +cic:/matita/algebra/monoids/is_left_inverse.con +cic:/matita/algebra/monoids/isSemiGroup_OF_Monoid.con +cic:/matita/algebra/monoids/isMonoid_rect.con +cic:/matita/algebra/monoids/isMonoid_rec.con +cic:/matita/algebra/monoids/isMonoid_ind.con +cic:/matita/algebra/monoids/isMonoid.ind +cic:/matita/algebra/monoids/e_is_right_unit.con +cic:/matita/algebra/monoids/e_is_left_unit.con +cic:/matita/algebra/monoids/e.con +cic:/matita/algebra/monoids/Type_OF_PreMonoid.con +cic:/matita/algebra/monoids/Type_OF_Monoid.con +cic:/matita/algebra/monoids/PreMonoid_rect.con +cic:/matita/algebra/monoids/PreMonoid_rec.con +cic:/matita/algebra/monoids/PreMonoid_ind.con +cic:/matita/algebra/monoids/PreMonoid.ind +cic:/matita/algebra/monoids/Monoid_rect.con +cic:/matita/algebra/monoids/Monoid_rec.con +cic:/matita/algebra/monoids/Monoid_ind.con +cic:/matita/algebra/monoids/Monoid.ind +cic:/matita/algebra/monoids/Magma_OF_Monoid.con +cic:/matita/algebra/semigroups/semigroup_properties.con +cic:/matita/algebra/semigroups/op_associative.con +cic:/matita/algebra/semigroups/op.con +cic:/matita/algebra/semigroups/magma.con +cic:/matita/algebra/semigroups/is_right_unit.con +cic:/matita/algebra/semigroups/is_left_unit_to_is_right_unit_to_eq.con +cic:/matita/algebra/semigroups/is_left_unit.con +cic:/matita/algebra/semigroups/isSemiGroup_rect.con +cic:/matita/algebra/semigroups/isSemiGroup_rec.con +cic:/matita/algebra/semigroups/isSemiGroup_ind.con +cic:/matita/algebra/semigroups/isSemiGroup.ind +cic:/matita/algebra/semigroups/carrier.con +cic:/matita/algebra/semigroups/Type_OF_SemiGroup.con +cic:/matita/algebra/semigroups/SemiGroup_rect.con +cic:/matita/algebra/semigroups/SemiGroup_rec.con +cic:/matita/algebra/semigroups/SemiGroup_ind.con +cic:/matita/algebra/semigroups/SemiGroup.ind +cic:/matita/algebra/semigroups/Magma_rect.con +cic:/matita/algebra/semigroups/Magma_rec.con +cic:/matita/algebra/semigroups/Magma_ind.con +cic:/matita/algebra/semigroups/Magma.ind +cic:/matita/datatypes/bool/true_to_true_to_andb_true.con +cic:/matita/datatypes/bool/orb_sym.con +cic:/matita/datatypes/bool/orb_elim.con +cic:/matita/datatypes/bool/orb.con +cic:/matita/datatypes/bool/notb_notb.con +cic:/matita/datatypes/bool/notb_elim.con +cic:/matita/datatypes/bool/notb.con +cic:/matita/datatypes/bool/not_eq_true_false.con +cic:/matita/datatypes/bool/injective_notb.con +cic:/matita/datatypes/bool/if_then_else.con +cic:/matita/datatypes/bool/bool_to_decidable_eq.con +cic:/matita/datatypes/bool/bool_rect.con +cic:/matita/datatypes/bool/bool_rec.con +cic:/matita/datatypes/bool/bool_ind.con +cic:/matita/datatypes/bool/bool_elim.con +cic:/matita/datatypes/bool/bool.ind +cic:/matita/datatypes/bool/andb_true_true_r.con +cic:/matita/datatypes/bool/andb_true_true.con +cic:/matita/datatypes/bool/andb_sym.con +cic:/matita/datatypes/bool/andb_elim.con +cic:/matita/datatypes/bool/andb_assoc.con +cic:/matita/datatypes/bool/andb.con +cic:/matita/datatypes/bool/and_true.con +cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con +cic:/matita/datatypes/compare/compare_rect.con +cic:/matita/datatypes/compare/compare_rec.con +cic:/matita/datatypes/compare/compare_invert.con +cic:/matita/datatypes/compare/compare_ind.con +cic:/matita/datatypes/compare/compare.ind +cic:/matita/datatypes/constructors/void_rect.con +cic:/matita/datatypes/constructors/void_rec.con +cic:/matita/datatypes/constructors/void_ind.con +cic:/matita/datatypes/constructors/void.ind +cic:/matita/datatypes/constructors/unit_rect.con +cic:/matita/datatypes/constructors/unit_rec.con +cic:/matita/datatypes/constructors/unit_ind.con +cic:/matita/datatypes/constructors/unit.ind +cic:/matita/datatypes/constructors/snd.con +cic:/matita/datatypes/constructors/option_rect.con +cic:/matita/datatypes/constructors/option_rec.con +cic:/matita/datatypes/constructors/option_ind.con +cic:/matita/datatypes/constructors/option.ind +cic:/matita/datatypes/constructors/fst.con +cic:/matita/datatypes/constructors/eq_pair_fst_snd.con +cic:/matita/datatypes/constructors/Sum_rect.con +cic:/matita/datatypes/constructors/Sum_rec.con +cic:/matita/datatypes/constructors/Sum_ind.con +cic:/matita/datatypes/constructors/Sum.ind +cic:/matita/datatypes/constructors/Prod_rect.con +cic:/matita/datatypes/constructors/Prod_rec.con +cic:/matita/datatypes/constructors/Prod_ind.con +cic:/matita/datatypes/constructors/Prod.ind +cic:/matita/decidable_kit/decidable/reflect_rect.con +cic:/matita/decidable_kit/decidable/reflect_rec.con +cic:/matita/decidable_kit/decidable/reflect_inv.con +cic:/matita/decidable_kit/decidable/reflect_ind.con +cic:/matita/decidable_kit/decidable/reflect.ind +cic:/matita/decidable_kit/decidable/prove_reflect.con +cic:/matita/decidable_kit/decidable/p2bT.con +cic:/matita/decidable_kit/decidable/p2bF.con +cic:/matita/decidable_kit/decidable/orbP.con +cic:/matita/decidable_kit/decidable/orbC.con +cic:/matita/decidable_kit/decidable/orb.con +cic:/matita/decidable_kit/decidable/negbP.con +cic:/matita/decidable_kit/decidable/negb.con +cic:/matita/decidable_kit/decidable/ltb_refl.con +cic:/matita/decidable_kit/decidable/ltb_n_Sm.con +cic:/matita/decidable_kit/decidable/ltbW.con +cic:/matita/decidable_kit/decidable/ltbP.con +cic:/matita/decidable_kit/decidable/ltb.con +cic:/matita/decidable_kit/decidable/ltW.con +cic:/matita/decidable_kit/decidable/ltS.con +cic:/matita/decidable_kit/decidable/ltS'.con +cic:/matita/decidable_kit/decidable/leb_refl.con +cic:/matita/decidable_kit/decidable/leb_eqb.con +cic:/matita/decidable_kit/decidable/lebW.con +cic:/matita/decidable_kit/decidable/lebP.con +cic:/matita/decidable_kit/decidable/idP.con +cic:/matita/decidable_kit/decidable/eq_to_bool.con +cic:/matita/decidable_kit/decidable/congr_S.con +cic:/matita/decidable_kit/decidable/bool_to_eq.con +cic:/matita/decidable_kit/decidable/b2pT.con +cic:/matita/decidable_kit/decidable/b2pF.con +cic:/matita/decidable_kit/decidable/andbPF.con +cic:/matita/decidable_kit/decidable/andbP.con +cic:/matita/decidable_kit/decidable/andb.con +cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con +cic:/matita/decidable_kit/eqtype/sval.con +cic:/matita/decidable_kit/eqtype/sub_eqType.con +cic:/matita/decidable_kit/eqtype/sprop.con +cic:/matita/decidable_kit/eqtype/sort_OF_nat.con +cic:/matita/decidable_kit/eqtype/sort_OF_bool.con +cic:/matita/decidable_kit/eqtype/sort.con +cic:/matita/decidable_kit/eqtype/sigma_rect.con +cic:/matita/decidable_kit/eqtype/sigma_rec.con +cic:/matita/decidable_kit/eqtype/sigma_ind.con +cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con +cic:/matita/decidable_kit/eqtype/sigma.ind +cic:/matita/decidable_kit/eqtype/option_eqType.con +cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con +cic:/matita/decidable_kit/eqtype/ocmpP.con +cic:/matita/decidable_kit/eqtype/ocmp.con +cic:/matita/decidable_kit/eqtype/nat_eqType.con +cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con +cic:/matita/decidable_kit/eqtype/in_sub_rect.con +cic:/matita/decidable_kit/eqtype/in_sub_rec.con +cic:/matita/decidable_kit/eqtype/in_sub_inv.con +cic:/matita/decidable_kit/eqtype/in_sub_ind.con +cic:/matita/decidable_kit/eqtype/in_sub_eq.con +cic:/matita/decidable_kit/eqtype/in_sub.ind +cic:/matita/decidable_kit/eqtype/if_p.con +cic:/matita/decidable_kit/eqtype/eqbP.con +cic:/matita/decidable_kit/eqtype/eq_compatible.con +cic:/matita/decidable_kit/eqtype/eqType_rect.con +cic:/matita/decidable_kit/eqtype/eqType_rec.con +cic:/matita/decidable_kit/eqtype/eqType_ind.con +cic:/matita/decidable_kit/eqtype/eqType_decidable.con +cic:/matita/decidable_kit/eqtype/eqType.ind +cic:/matita/decidable_kit/eqtype/eqP.con +cic:/matita/decidable_kit/eqtype/cmp_refl.con +cic:/matita/decidable_kit/eqtype/cmpP.con +cic:/matita/decidable_kit/eqtype/cmpC.con +cic:/matita/decidable_kit/eqtype/cmp.con +cic:/matita/decidable_kit/eqtype/bool_eqType.con +cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con +cic:/matita/decidable_kit/eqtype/bcmpP.con +cic:/matita/decidable_kit/eqtype/bcmp.con +cic:/matita/decidable_kit/list_aux/mem.con +cic:/matita/decidable_kit/list_aux/list_eqType.con +cic:/matita/decidable_kit/list_aux/lcmp_length.con +cic:/matita/decidable_kit/list_aux/lcmpP.con +cic:/matita/decidable_kit/list_aux/lcmp.con +cic:/matita/decidable_kit/list_aux/count.con +cic:/matita/decidable_kit/streicher/stepH.con +cic:/matita/decidable_kit/streicher/step.con +cic:/matita/decidable_kit/streicher/pirrel.con +cic:/matita/decidable_kit/streicher/nu_k.con +cic:/matita/decidable_kit/streicher/nu_inv.con +cic:/matita/decidable_kit/streicher/nu.con +cic:/matita/decidable_kit/streicher/decT.con +cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con +cic:/matita/decidable_kit/streicher/cancel.con +cic:/matita/demo/realisability/type_OF_SP.con +cic:/matita/demo/realisability/true_impl_realized.con +cic:/matita/demo/realisability/sigma_rect.con +cic:/matita/demo/realisability/sigma_rec.con +cic:/matita/demo/realisability/sigma_ind.con +cic:/matita/demo/realisability/sigma.ind +cic:/matita/demo/realisability/realized.con +cic:/matita/demo/realisability/pi2.con +cic:/matita/demo/realisability/pi1.con +cic:/matita/demo/realisability/modr.con +cic:/matita/demo/realisability/id_axiom.con +cic:/matita/demo/realisability/extraction.con +cic:/matita/demo/realisability/elim_abs.con +cic:/matita/demo/realisability/cut.con +cic:/matita/demo/realisability/correct2.con +cic:/matita/demo/realisability/correct.con +cic:/matita/demo/realisability/and_i.con +cic:/matita/demo/realisability/SP_rect.con +cic:/matita/demo/realisability/SP_rec.con +cic:/matita/demo/realisability/SP_ind.con +cic:/matita/demo/realisability/SP.ind +cic:/matita/demo/realisability/Prop_OF_SP.con +cic:/matita/higher_order_defs/functions/symmetric2.con +cic:/matita/higher_order_defs/functions/symmetric.con +cic:/matita/higher_order_defs/functions/surjective.con +cic:/matita/higher_order_defs/functions/monotonic.con +cic:/matita/higher_order_defs/functions/injective.con +cic:/matita/higher_order_defs/functions/eq_f_g_h.con +cic:/matita/higher_order_defs/functions/distributive2.con +cic:/matita/higher_order_defs/functions/distributive.con +cic:/matita/higher_order_defs/functions/compose.con +cic:/matita/higher_order_defs/functions/associative.con +cic:/matita/higher_order_defs/ordering/antisymmetric.con +cic:/matita/higher_order_defs/relations/transitive.con +cic:/matita/higher_order_defs/relations/tight_apart.con +cic:/matita/higher_order_defs/relations/symmetric.con +cic:/matita/higher_order_defs/relations/relation.con +cic:/matita/higher_order_defs/relations/reflexive.con +cic:/matita/higher_order_defs/relations/irreflexive.con +cic:/matita/higher_order_defs/relations/cotransitive.con +cic:/matita/higher_order_defs/relations/antisymmetric.con +cic:/matita/list/list/x3.con +cic:/matita/list/list/x2.con +cic:/matita/list/list/x1.con +cic:/matita/list/list/tmp.con +cic:/matita/list/list/tail_demod2.con +cic:/matita/list/list/tail_demod1.con +cic:/matita/list/list/tail.con +cic:/matita/list/list/permutation_inv.con +cic:/matita/list/list/permutation_ind.con +cic:/matita/list/list/permutation.ind +cic:/matita/list/list/permut1_inv.con +cic:/matita/list/list/permut1_ind.con +cic:/matita/list/list/nth.con +cic:/matita/list/list/nil_cons.con +cic:/matita/list/list/map_foldr2.con +cic:/matita/list/list/map_foldr1.con +cic:/matita/list/list/map_demod2.con +cic:/matita/list/list/map_demod1.con +cic:/matita/list/list/map.con +cic:/matita/list/list/list_rect.con +cic:/matita/list/list/list_rec.con +cic:/matita/list/list/list_ind2.con +cic:/matita/list/list/list_ind.con +cic:/matita/list/list/list.ind +cic:/matita/list/list/length.con +cic:/matita/list/list/len_demod2.con +cic:/matita/list/list/len_demod1.con +cic:/matita/list/list/le_length_filter.con +cic:/matita/list/list/iota_demod2.con +cic:/matita/list/list/iota_demod1.con +cic:/matita/list/list/iota.con +cic:/matita/list/list/id_list.con +cic:/matita/list/list/foldr.con +cic:/matita/list/list/filter_demod2.con +cic:/matita/list/list/filter_demod1.con +cic:/matita/list/list/filter.con +cic:/matita/list/list/eq_map.con +cic:/matita/list/list/cons_append_commute.con +cic:/matita/list/list/associative_append.con +cic:/matita/list/list/append_nil.con +cic:/matita/list/list/append_demod2.con +cic:/matita/list/list/append_demod1.con +cic:/matita/list/list/append_cons.con +cic:/matita/list/list/append.con +cic:/matita/logic/coimplication/iff_trans.con +cic:/matita/logic/coimplication/iff_sym.con +cic:/matita/logic/coimplication/iff_refl.con +cic:/matita/logic/coimplication/iff_intro.con +cic:/matita/logic/coimplication/Iff.con +cic:/matita/logic/connectives/proj2.con +cic:/matita/logic/connectives/proj1.con +cic:/matita/logic/connectives/iff.con +cic:/matita/logic/connectives/ex_ind.con +cic:/matita/logic/connectives/ex2_ind.con +cic:/matita/logic/connectives/ex2.ind +cic:/matita/logic/connectives/ex.ind +cic:/matita/logic/connectives/decidable.con +cic:/matita/logic/connectives/absurd.con +cic:/matita/logic/connectives/True_rect.con +cic:/matita/logic/connectives/True_rec.con +cic:/matita/logic/connectives/True_ind.con +cic:/matita/logic/connectives/True.ind +cic:/matita/logic/connectives/Or_ind.con +cic:/matita/logic/connectives/Or_ind'.con +cic:/matita/logic/connectives/Or.ind +cic:/matita/logic/connectives/Not.con +cic:/matita/logic/connectives/False_rect.con +cic:/matita/logic/connectives/False_rec.con +cic:/matita/logic/connectives/False_ind.con +cic:/matita/logic/connectives/False.ind +cic:/matita/logic/connectives/And_rect.con +cic:/matita/logic/connectives/And_rec.con +cic:/matita/logic/connectives/And_ind.con +cic:/matita/logic/connectives/And.ind +cic:/matita/logic/connectives2/transitive_iff.con +cic:/matita/logic/connectives2/symmetric_iff.con +cic:/matita/logic/connectives2/reflexive_iff.con +cic:/matita/logic/equality/transitive_eq.con +cic:/matita/logic/equality/trans_sym_eq.con +cic:/matita/logic/equality/trans_eq.con +cic:/matita/logic/equality/symmetric_eq.con +cic:/matita/logic/equality/sym_eq.con +cic:/matita/logic/equality/reflexive_eq.con +cic:/matita/logic/equality/nu_left_inv.con +cic:/matita/logic/equality/nu_inv.con +cic:/matita/logic/equality/nu_constant.con +cic:/matita/logic/equality/nu.con +cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con +cic:/matita/logic/equality/eq_rect.con +cic:/matita/logic/equality/eq_rect'.con +cic:/matita/logic/equality/eq_rec.con +cic:/matita/logic/equality/eq_ind.con +cic:/matita/logic/equality/eq_f2.con +cic:/matita/logic/equality/eq_f.con +cic:/matita/logic/equality/eq_f'.con +cic:/matita/logic/equality/eq_elim_r.con +cic:/matita/logic/equality/eq_elim_r'.con +cic:/matita/logic/equality/eq_elim_r''.con +cic:/matita/logic/equality/eq_OF_eq2.con +cic:/matita/logic/equality/eq_OF_eq1.con +cic:/matita/logic/equality/eq_OF_eq.con +cic:/matita/logic/equality/eq.ind +cic:/matita/logic/equality/comp.con +cic:/matita/technicalities/setoids/variance_rect.con +cic:/matita/technicalities/setoids/variance_rec.con +cic:/matita/technicalities/setoids/variance_of_argument_class.con +cic:/matita/technicalities/setoids/variance_ind.con +cic:/matita/technicalities/setoids/variance.ind +cic:/matita/technicalities/setoids/rewrite_direction_rect.con +cic:/matita/technicalities/setoids/rewrite_direction_rec.con +cic:/matita/technicalities/setoids/rewrite_direction_ind.con +cic:/matita/technicalities/setoids/rewrite_direction.ind +cic:/matita/technicalities/setoids/relation_of_relation_class.con +cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con +cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con +cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con +cic:/matita/technicalities/setoids/relation_class_of_argument_class.con +cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con +cic:/matita/technicalities/setoids/product_of_arguments.con +cic:/matita/technicalities/setoids/opposite_direction_idempotent.con +cic:/matita/technicalities/setoids/opposite_direction.con +cic:/matita/technicalities/setoids/nelistT_rect.con +cic:/matita/technicalities/setoids/nelistT_rec.con +cic:/matita/technicalities/setoids/nelistT_ind.con +cic:/matita/technicalities/setoids/nelistT.ind +cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con +cic:/matita/technicalities/setoids/morphism_theory_of_function.con +cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con +cic:/matita/technicalities/setoids/make_compatibility_goal.con +cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con +cic:/matita/technicalities/setoids/interp_relation_class_list.con +cic:/matita/technicalities/setoids/interp.con +cic:/matita/technicalities/setoids/impl_trans.con +cic:/matita/technicalities/setoids/impl_refl.con +cic:/matita/technicalities/setoids/impl.con +cic:/matita/technicalities/setoids/get_rewrite_direction.con +cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con +cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con +cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con +cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con +cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con +cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con +cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con +cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con +cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con +cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind +cic:/matita/technicalities/setoids/carrier_of_relation_class.con +cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con +cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con +cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con +cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con +cic:/matita/technicalities/setoids/apply_morphism.con +cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con +cic:/matita/technicalities/setoids/X_Relation_Class_rect.con +cic:/matita/technicalities/setoids/X_Relation_Class_rec.con +cic:/matita/technicalities/setoids/X_Relation_Class_ind.con +cic:/matita/technicalities/setoids/X_Relation_Class.ind +cic:/matita/technicalities/setoids/Relation_Class.con +cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con +cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con +cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con +cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind +cic:/matita/technicalities/setoids/Morphism_Theory_rect.con +cic:/matita/technicalities/setoids/Morphism_Theory_rec.con +cic:/matita/technicalities/setoids/Morphism_Theory_ind.con +cic:/matita/technicalities/setoids/Morphism_Theory.ind +cic:/matita/technicalities/setoids/Morphism_Context_rect2.con +cic:/matita/technicalities/setoids/Morphism_Context_rect.con +cic:/matita/technicalities/setoids/Morphism_Context_rec.con +cic:/matita/technicalities/setoids/Morphism_Context_inv.con +cic:/matita/technicalities/setoids/Morphism_Context_ind.con +cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con +cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con +cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con +cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con +cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con +cic:/matita/technicalities/setoids/Morphism_Context.ind +cic:/matita/technicalities/setoids/Impl_Relation_Class.con +cic:/matita/technicalities/setoids/Iff_Relation_Class.con +cic:/matita/technicalities/setoids/Function.con +cic:/matita/technicalities/setoids/Compat.con +cic:/matita/technicalities/setoids/Arguments.con +cic:/matita/technicalities/setoids/Argument_Class.con +cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con +cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con +cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con +cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind +cic:/matita/tests/XXX.ind diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 8aae86b89..87f9580da 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -7,13 +7,34 @@ let _ = prerr_endline ("End: " ^ NUri.string_of_uri s)); NCicPp.set_ppterm NCicPp.trivial_pp_term; Helm_registry.load_from "conf.xml"; - let u = UriManager.uri_of_string Sys.argv.(1) in - let _,o = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in - try NCicTypeChecker.typecheck_obj o - with - | NCicTypeChecker.AssertFailure s - | NCicTypeChecker.TypeCheckerFailure s as e -> - prerr_endline (Lazy.force s); raise e - | CicEnvironment.Object_not_found s -> - prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s) + let alluris = + try [Sys.argv.(1)] + with Invalid_argument _ -> + let r = ref [] in + let ic = open_in "alluris.txt" in + try while true do r := input_line ic :: !r; done; [] + with _ -> List.rev !r + in +(* uncomment to obtain the list of uris + let uri_re = Str.regexp ".*\\(ind\\|var\\|con\\)$" in + let uris = Http_getter.getalluris () in + let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in + let oc = open_out "alluris.txt" in + List.iter (fun s -> output_string oc (s^"\n")) alluris; + close_out oc; exit 0; +*) + List.iter (fun uu -> + prerr_endline ("************* INIZIO **************** " ^ uu); + let u = UriManager.uri_of_string uu in + let _,o = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in + try + NCicTypeChecker.typecheck_obj o; + prerr_endline ("************* FINE ****************" ^ uu); + with + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s as e -> + prerr_endline (Lazy.force s); raise e + | CicEnvironment.Object_not_found s -> + prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)) + alluris ;; -- 2.39.2