Skip to content
Snippets Groups Projects
Commit b5887b24 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/wp/tac-induction' into 'master'

Remove useless subtitution in Induction tactic

See merge request frama-c/frama-c!3526
parents 98678b60 a96d17b6
No related branches found
No related tags found
No related merge requests found
......@@ -53,7 +53,7 @@ let process value n0 sequent =
let seq, goal = Conditions.map_sequent (F.p_subst sigma) sequent in
let hind = ref [] in
let seq = filter_seq n hind seq in
let goal_n = F.p_hyps !hind @@ F.p_subst sigma goal in
let goal_n = F.p_hyps !hind goal in
let goal_i = F.p_subst_var n vi goal_n in
(* Base: n = n0 *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment