Hugo Herbelin (Jul 30 2021 at 15:14): Hugo Herbelin (Jul 30 2021 at 15:14):Does anyone know 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.
Matthieu Sozeau (Sep 08 2021 at 15:05):It must be produced by setoid_rewrite
Last updated: Oct 13 2024 at 01:02 UTC