Commit 7e7ed428 authored by Beta Ziliani's avatar Beta Ziliani

adapting to last change in Mtac2/master

parent c5ffd28c
......@@ -371,7 +371,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.Sorts.SType ng in
let g' := Goal 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