search

coq-community / trocq

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
http://coq-community.org/trocq/
GNU Lesser General Public License v3.0
18 stars 3 forks source link

Interaction of the `trocq` tactic with Coq #21

Open ecranceMERCE opened 9 months ago

ecranceMERCE commented 9 months ago

The definition of the trocq tactic makes use of elaboration, then typechecking, then conversion:

https://github.com/coq-community/trocq/blob/95f083ad0b3bca87324437d835b5957b9bd6a6cd/theories/Param.v#L154-L157

After that, refine is called without checks. Why are all these steps required, and why was the work done by hand on the Elpi side instead of delegating the checks to refine?

CohenCyril commented 9 months ago

CC @gares

gares commented 9 months ago

The current API does not report errors nicely as you do here. Maybe it should.