search

SkySkimmer / coq-ltac2-compiler

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

Put back hardcoded primitives #1

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

This reverts commit 4fe18d40dee91c50b7bf62afa427d3f6739b893e.

ie put back 2ead24641f13feb5b79b903ccc0d1d74be73dfbe

Waiting for https://github.com/coq/coq/pull/17730