diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index 0edcc8430adf32d77818ab7f4fc51f6f5345aae4..550a6caed14f304d3c20aae06570cec7a5b2f9ed 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -198,6 +198,7 @@ class mkcomposer
           Wutil.on filter (fun f -> wvalid <- f) ;
           Wutil.on range (fun r -> ranged <- r) ;
           ignore vmin ; ignore vmax ;
+          self#updated
         end
   end
 
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 8684a6011d7cc0a3cf640213a41e25a43e883fba..630d6be6e535abfb3efd0624598165bb5c46d674 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -98,7 +98,13 @@ class induction =
       | _ ->
           None
 
-    method select _feedback (s : Tactical.selection) =
+    method select feedback (s : Tactical.selection) =
+      begin match self#get_field vbase with
+        | Empty ->
+            self#set_field vbase (Tactical.int 0) ;
+            feedback#update_field vbase
+        | _ -> ()
+      end ;
       let value = Tactical.selected s in
       if F.is_int value then
         match self#get_base () with