more fix removed from types

[helm.git] / 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
index 84385385cffd7b9358cdd0588899e7cf380bd830..4692a4f143ee5b80b662007c80d1499118f47916 100644 (file)
--- a/helm/software/components/ng_kernel/alluris.txt
+++ b/helm/software/components/ng_kernel/alluris.txt
@@ -1,3 +1,59 @@
+cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
+cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
+cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/appA.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
+cic:/matita/algebra/CoRN/SetoidFun/UR.con
+cic:/matita/algebra/CoRN/SetoidFun/UQ.con
+cic:/matita/algebra/CoRN/SetoidFun/UP.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
+cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/Inv.con
+cic:/matita/algebra/CoRN/SetoidFun/Fid.con
+cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
+cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
+cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/BR.con
+cic:/matita/algebra/CoRN/SetoidFun/BQ.con
+cic:/matita/algebra/CoRN/SetoidFun/BP.con
+cic:/matita/algebra/CoRN/SetoidFun/Astar.con
+cic:/matita/demo/realisability/correct2.con
+cic:/matita/demo/realisability/correct.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
 cic:/matita/demo/realisability/type_OF_SP.con
 cic:/matita/demo/realisability/true_impl_realized.con
 cic:/matita/demo/realisability/sigma_rect.con
@@ -2057,65 +2113,6 @@ 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
-# -- fine --
-# # the same fix in different contexts has different lamb-lifted counterpart + generative fix
-# cic:/matita/demo/realisability/correct2.con
-# cic:/matita/demo/realisability/correct.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
-# # depending on the previous
-# cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
-# cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
-# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
-# cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
-# cic:/matita/algebra/CoRN/SetoidFun/appA.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
-# cic:/matita/algebra/CoRN/SetoidFun/UR.con
-# cic:/matita/algebra/CoRN/SetoidFun/UQ.con
-# cic:/matita/algebra/CoRN/SetoidFun/UP.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
-# cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
-# cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
-# cic:/matita/algebra/CoRN/SetoidFun/Inv.con
-# cic:/matita/algebra/CoRN/SetoidFun/Fid.con
-# cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
-# cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
-# cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
-# cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
-# cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
-# cic:/matita/algebra/CoRN/SetoidFun/BR.con
-# cic:/matita/algebra/CoRN/SetoidFun/BQ.con
-# cic:/matita/algebra/CoRN/SetoidFun/BP.con
-# cic:/matita/algebra/CoRN/SetoidFun/Astar.con
 # # mutual fix
 # cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
 # # depending on the previous