Commit 261f7532 authored by Janno's avatar Janno

Fix error resulting from goal_dep merge.

parent ca9b8e70
......@@ -377,7 +377,7 @@ Definition simpl_subst : tactic :=
(* rewrite <-(W.to_expr_subst x);; *)
(fun g =>
ng <- M.evar (C (W.to_expr (W.subst x er' e')));
let g' := Goal Sorts.S.SType ng in
let g' := GoalOut Sorts.S.SType ng in
T.exact (match W.to_expr_subst x er' e' in _ = R return C R with | eq_refl => ng end) g;;
M.ret [m: (m: tt, g')]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment