Murali Vijayaraghavan
Results
51
comments of
Murali Vijayaraghavan
Just adding another example. Something that has been plaguing me since ltac:() was introduced, just like interpretation scopes. ``` Definition y := ((ltac:(abstract (exact (1: nat)))): nat). Print y. (*...