Type related failures fixed

diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt
index 4692a4f143ee5b80b662007c80d1499118f47916..444ee8e6071ac01cc1b0513fa26d95675e07276b 100644 (file)
--- a/helm/software/components/ng_kernel/alluris.txt
+++ b/helm/software/components/ng_kernel/alluris.txt
@@ -2113,6 +2113,76 @@ 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/relation_of_product_of_arguments.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
 # # mutual fix
 # cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
 # # depending on the previous
@@ -2135,74 +2205,3 @@ cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.c
 # cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
 # cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
 # cic:/matita/demo/propositional_sequent_calculus/Formula.ind
-# # universe inferece missing
-# cic:/matita/technicalities/setoids/relation_of_product_of_arguments.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