Fix Class_tactics.run_on_goals setting incorrect typeclass evars

Fix coq#18127
SkySkimmer · Oct 5, 2023 · 6d5365f · 6d5365f
1 parent 4429d4b
commit 6d5365f
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
@@ -1041,7 +1041,7 @@ module Search = struct
     in
     let nongoals' =
       Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
-          | Some ev' -> Evar.Set.add ev acc
+          | Some ev -> Evar.Set.add ev acc
           | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm')
     in
     (* FIXME: the need to merge metas seems to come from this being called

diff --git a/test-suite/bugs/bug_18127.v b/test-suite/bugs/bug_18127.v
@@ -0,0 +1,10 @@
+Class Class1 (hom : Type) (c : hom) : Type := {
+    var1 : hom -> Type;
+    var2 : hom;
+}.
+
+Class Class2 {h c} (C : Class1 h c) (fmap : h -> h) := {
+    var3 : var1 (fmap var2);
+}.
+
+Definition var3_cast : forall {h c C fm}, Class2 C fm -> var1 (fm var2) := @var3.