diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 2168784bca217769aec19e2f63bca928382994b3..7bbe267f4a216bdb8780b32faa3f6ac7d7de2d9d 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -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 *)