coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] tactical to get the goal (reified) on applying a tactic

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] tactical to get the goal (reified) on applying a tactic
Date: Thu, 17 Dec 2020 11:09:01 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f43.google.com
Ironport-phdr: 9a23:XKtbOh2DAtrmQFF/smDT+DRfVm0co7zxezQtwd8ZseIfK/ad9pjvdHbS+e9qxAeQG9mCtLQd2rad4v2ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalvIBiyogjduc0bjIt/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6JVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOtEtIb9p1oOrQC+BQayB+Pk1yNFhnns0q08zusqDAbL0xY7ENIOsXTUt9X1O7kRUeyv1qbIyy/Mb/VL1jvn6YjIcwwhof6XULJ/dMre00gvFwffglqMrozlOiqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hh5fJiI8L113J+ip3zZsrKdC2VkJ2YsKpHZVQuS2EOIZ7RsEvT3xqtSsnyrAIuZy2cSsIxZg72RLTdf+KfouG7x/lSe2fLzB4hHd/d7K+gRa/6VSvyurmVsmyzllKqi5FnsPSuX8Qyhze7NWMRPhl/kq5xzqDywTe5vtHLE00j6bXNp8sz78qmpccv0nOGDL9ll/sg6+MbEok//Cl6+T5bbXioZ+RL4p0hRv/MqQqg8C/AOM4PhUXU2iV9umx2qfv/UL+QLVNgf02lrfWvIrGKsQco661Gw5V0oA95BajFzqqzsgUkH0dIF9GeB+LlZXlNlDPLfziAvqyjUygkDJxyPDHOr3hDI/NLn/GkLr5Z7ly8E5cyAsozdBf+Z1UCasNL+j1WkDrstzXEwU1Mw21w+b7B9VwzYweWWeVDa+YNKPeq0OH5uUqI+WUfo8apC79K+Q55/7plXI2hVgdfbCw0ZQLbHC4A+9pLl6CYXvsh9cBCX0FshA/TOzskl2CUCRca2y8X6ImtXkHD9etCp6GTYSwivTV1yCiW5ZSe2puC1aWEH6ueZ/SCNkWbyfHC8VhkycEWLvpYoko0x3m4Abwy7t8LufXvCQevJTvktl0++L7mhQ79DgyBMOYhTLeB1pol38FEmdllJt0plZwnw/ajfpIxsdAHNkW3MtnFx8gPMeFneN/AtH2HAnGe4XREQf0cpCdGTg0C+kJ7ZoLakd5Fc+li0majSWvCr4R0beMAc5tq/+O7z3KP894jk3++uwhgl0hGJYdMGSngut+8FGWCdKS1UqekKmueOIX2yufrGo=

Do/can we have some tactic `getGoalOn tac` such that it returns a reification (Gallina or Ltac data structure) of goals after applying tac on the current goal, without changing the current goal?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] tactical to get the goal (reified) on applying a tactic, Abhishek Anand, 12/17/2020