Interaction of the trocq tactic with Coq

[ecranceMERCE]

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

trocq/theories/Param.v

Lines 154 to 157 in 95f083a

	std.assert-ok! (coq.elaborate-skeleton FinalProof G EFinalProof) "proof elaboration error",
	std.assert-ok! (coq.typecheck EFinalProof G2) "proof typechecking error",
	std.assert-ok! (coq.unify-leq G2 G) "goal unification error",
	refine.no_check EFinalProof InitialGoal NewGoals

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]

CC @gares

[gares]

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