Stream: Coq devs & plugin devs

Topic: Naming evars produced by setoid rewrite


view this post on Zulip Hugo Herbelin (Jul 30 2021 at 15:14):

Does anyone now which call to new_evar produces the evar in test bug_14239.v?

Require Import Setoid Morphisms.
Parameter reli : forall (dummy:unit)(R:relation unit), relation unit.
Parameter f g : unit -> unit.
Declare Instance c (dummy : unit) (R : relation unit) : Proper (reli dummy R ==> R) f.
Parameter H : forall (eq : relation unit) (a : unit), eq a a -> eq (g a) a.
Goal f (g tt) = tt.
rewrite H.
(* 2 goals
______________________________________(1/2)
f tt = tt
______________________________________(2/2)
reli ?Goal1 eq tt tt
*)

It seems to me that it would be more appealing that ?Goal1 is named ?dummy but I can't find the call to new_evar that produced it, so as to add it an VarInstance id source which will name it.

view this post on Zulip Matthieu Sozeau (Sep 08 2021 at 15:05):

It must be produced by setoid_rewrite


Last updated: Oct 16 2021 at 07:02 UTC