[wp] Induction tactic base defaults to 0

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
 

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