SkySkimmer / coq-ltac2-compiler

GNU Lesser General Public License v2.1
5 stars 0 forks source link

Translate non recursive let to nontac expr when possible #20

Closed SkySkimmer closed 12 months ago

SkySkimmer commented 12 months ago

Fix #16 (by being compatible with Tac2intern.is_value)

I'd like to have a more direct implementation than using is_nontac but it's not coming to me.