FissoreD / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
0 stars 0 forks source link

Create mapping coq evars -> elpi evar (to avoid typechecking while solving) #8

Closed FissoreD closed 1 month ago

FissoreD commented 1 month ago
  1. Given a goal $G$ with the list of evars $c_1...c_n$, build a list of elpi fresh variables $e_1...e_n$.
  2. The goal to analyse is $G'$ where each $c_i$ is replaced by $e_i$.
  3. Launch resolution on $G'$.
  4. When a solution is found, map back each $e_i$ to $c_i$

This variable replacement avoid the trigger of coq suspended evar.