Remove the TacComplete AST

It has always bothered me that there is an AST entry for `TacComplete` that has
no equivalent in syntax. Presumably, at some point, there was an intention for a
tactical `complete t`. Now, everyone just uses `solve [t]`, which was meant to
be equivalent to `first [complete t]`.

plugins/ltac/pptactic.ml

@@ -643,7 +643,6 @@ let pr_goal_selector ~toplevel s =
   let lorelse = 2
   let llet = 5
   let lfun = 5
-  let lcomplete = 1
   let labstract = 3
   let lmatch = 1
   let latom = 0
@@ -1027,8 +1026,6 @@ let pr_goal_selector ~toplevel s =
               keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
             | TacSolve tl ->
               keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
-            | TacComplete t ->
-              pr_tac (LevelLe lcomplete) t, lcomplete
             | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, ltactical
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom

plugins/ltac/tacexpr.ml

@@ -196,7 +196,6 @@ and 'a gen_tactic_expr_r =
       'a gen_tactic_expr *
       'a gen_tactic_expr array
   | TacFirst of 'a gen_tactic_expr list
-  | TacComplete of 'a gen_tactic_expr
   | TacSolve of 'a gen_tactic_expr list
   | TacTry of 'a gen_tactic_expr
   | TacOr of

plugins/ltac/tacexpr.mli

@@ -195,7 +195,6 @@ and 'a gen_tactic_expr_r =
       'a gen_tactic_expr *
       'a gen_tactic_expr array
   | TacFirst of 'a gen_tactic_expr list
-  | TacComplete of 'a gen_tactic_expr
   | TacSolve of 'a gen_tactic_expr list
   | TacTry of 'a gen_tactic_expr
   | TacOr of

plugins/ltac/tacintern.ml

@@ -663,7 +663,6 @@ and intern_tactic_seq onlytac ist tac =
       ist.ltacvars, CAst.make ?loc (TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2))
   | TacFirst l -> ist.ltacvars, CAst.make ?loc (TacFirst (List.map (intern_pure_tactic ist) l))
   | TacSolve l -> ist.ltacvars, CAst.make ?loc (TacSolve (List.map (intern_pure_tactic ist) l))
-  | TacComplete tac -> ist.ltacvars, CAst.make ?loc (TacComplete (intern_pure_tactic ist tac))
   | TacArg a -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
   | TacSelect (sel, tac) ->
       ist.ltacvars, CAst.make ?loc (TacSelect (sel, intern_pure_tactic ist tac))

plugins/ltac/tacinterp.ml

@@ -1196,7 +1196,6 @@ and eval_tactic_ist ist tac : unit Proofview.tactic =
       Tacticals.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
   | TacFirst l -> Tacticals.tclFIRST (List.map (interp_tactic ist) l)
   | TacSolve l -> Tacticals.tclSOLVE (List.map (interp_tactic ist) l)
-  | TacComplete tac -> Tacticals.tclCOMPLETE (interp_tactic ist tac)
   | TacArg _ -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
   | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac)
 

plugins/ltac/tacsubst.ml

@@ -216,7 +216,6 @@ and subst_tactic subst = CAst.map (function
       TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
   | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
   | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
-  | TacComplete tac -> TacComplete (subst_tactic subst tac)
   | TacArg a -> TacArg (subst_tacarg subst a)
   | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac)
 

plugins/ltac/tactic_debug.ml

@@ -355,7 +355,6 @@ let tac_loc tac =
   | TacThens _ -> "TacThens"
   | TacThens3parts _ -> "TacThens3parts"
   | TacFirst _ -> "TacFirst"
-  | TacComplete _ -> "TacComplete"
   | TacSolve _ -> "TacSolve"
   | TacTry _ -> "TacTry"
   | TacOr _ -> "TacOr"