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

Published 20 hours ago • verified publisher icon mattam82

Improve deplim etc...

Open thomas-lamiaux opened this issue 9 months ago • 1 comments
trafficstars

  • depelim should be an alias for dependent elimination?
  • improve return messages for noconf, depelim, dependent elim

thomas-lamiaux avatar Feb 18 '25 14:02 thomas-lamiaux

@yannl35133 does not agree that depelim should be an alias

thomas-lamiaux avatar Feb 18 '25 14:02 thomas-lamiaux