I am struggling with this error:

```
Flexible term outside pattern fragment:
X48 c0 c1 c2 (pglobal (const «...») «...»)
```

I think it comes from putting variables in a term, then abstracting the term w.r.t. an eigenvariable, then applying the resulting function to a term that is not a variable.

Is there an easy way to remove the non-eigenvariable terms from the scope of the variables? Like an automatic recursive `prune`

operation that would leave only the visible eigenvariables coming from the traversed binders? The only other options I have found to avoid this problem are:

- strictly give every type annotation everywhere in the term, but for some cases it is tedious;
- put a dummy eigenvariable and replace it with fresh variables everytime anything external is needed (
*e.g.*typechecking), but it is a lot of bureaucracy.

I think you found the root cause, if `F`

is an Elpi function over Coq terms and it contains a unification variable and `T`

is an arbitrary term, then `P = F T`

is a problematic term, it is outside the pattern fragment.

Now, the easiest way to pass a term like `P`

to Coq is to use the `@holes!`

option (it is taken by all APIs taking a term, IIRC).

Another one is to use `coq.elaborate`

. The former prunes, the latter simply ignores the arguments to the hole.

See https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html#outside-the-pattern-fragment and

https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L213-L231

Last updated: Jun 06 2023 at 21:01 UTC