fix: get_elem_tactic_trivial to not loop in the presence of mvars#5119
Merged
nomeata merged 1 commit intomasterfrom joachim/issue5061Aug 21, 2024
+34-1
get_elem_tactic_trivial to not loop in the presence of mvars#5119