let compute_goal_sort_tac = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, goalsort = typeof status (ctx_of goalty) goalty in
+ let goalsort = fix_sorts goalsort in
sort := Some goalsort;
exec id_tac status goal)
in
| _ -> assert false
in
let name =
- match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix
+ match dir with
+ `LeftToRight -> "eq" ^ suffix ^ "_r"
+ | `RightToLeft -> "eq" ^ suffix
in
block_tac
[ select_tac ~where ~job:(`Substexpand 1) true;