coq.elaborate-skeleton abstracts over evars #919

Activity

1. gares commented on Oct 28, 2025

   

   gares

   on Oct 28, 2025

   Contributor

   More actions

   The culprit is
   

   coq-elpi/src/rocq_elpi_utils.ml

   Line 618 in 8fcbf23

   | Evar _ -> mkGHole

   To do this properly one needs:

   • add an option, eg @no-holes!
   • since we do not want to lose non-linearity carry a map Evar.t -> Evar.t
   • since we do not want to modify the input term create a new evar every time we encounter one, and add it to the map above and to sigma
2. Tragicus commented on Nov 6, 2025

   

   Tragicus

   on Nov 6, 2025

   ContributorAuthor

   More actions

   I am not sure I understand the point of the option. Should we not always turn identical evars into identical holes?
3. gares commented on Nov 7, 2025

   

   gares

   on Nov 7, 2025

   Contributor

   More actions

   Maybe it is the best default, but it is not how it works currently and if we don't have the option we break code. Let's see how CI goeas.