Coq-Equations icon indicating copy to clipboard operation
Coq-Equations copied to clipboard

Generalize funelim to take into account parameters of polymorphic

Open mattam82 opened this issue 7 years ago • 0 comments

functions which shouldn't be generalized blindly. In general the strategy for generalizing the arguments of the function for functional elimination seems suboptimal. It might try to generalize arguments that are dependent (appear elsewhere in the goal) resulting in ill-typed generalizations. We might need the proper second_order_abstraction procedure of unifall to find the most general typable generalization of the goal w.r.t the arguments of the function to solve this problem.

mattam82 avatar Nov 21 '17 23:11 mattam82