Deprecate "end tac" ("...")

dev/ci/user-overlays/20917-SkySkimmer-depr-dots.sh

@@ -0,0 +1,5 @@
+overlay tactician https://github.com/SkySkimmer/coq-tactician depr-dots 20917
+
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp depr-dots 20917
+
+overlay vsrocq https://github.com/SkySkimmer/vsrocq depr-dots 20917

doc/tools/docgram/common.edit_mlg

@@ -1743,7 +1743,7 @@ tactic_mode: [
 (* todo: make sure to document this production! *)
 (* deleting to allow splicing query_command into command *)
 | DELETE OPT ltac_selector OPT ltac_info tactic ltac_use_default
-| DELETE "par" ":" OPT ltac_info tactic ltac_use_default
+| DELETE "par" ":" OPT ltac_info tactic "."
 (* Ignore attributes (none apply) and "...". *)
 | ltac_info tactic
 | MOVETO command ltac_info tactic

doc/tools/docgram/fullGrammar

@@ -2311,7 +2311,7 @@ tactic_mode: [
 | subprf
 | OPT toplevel_selector subprf_with_selector
 | OPT ltac_selector OPT ltac_info tactic ltac_use_default
-| "par" ":" OPT ltac_info tactic ltac_use_default
+| "par" ":" OPT ltac_info tactic "."
 ]
 
 ltac_selector: [
@@ -3332,7 +3332,7 @@ ltac2_use_default: [
 
 tac2mode: [
 | OPT ltac2_selector ltac2_expr6 ltac2_use_default      (* ltac2 plugin *)
-| "par" ":" ltac2_expr6 ltac2_use_default      (* ltac2 plugin *)
+| "par" ":" ltac2_expr6 "."      (* ltac2 plugin *)
 | subprf      (* ltac2 plugin *)
 | OPT toplevel_selector subprf_with_selector      (* ltac2 plugin *)
 ]

plugins/ltac/g_ltac.mlg

@@ -323,13 +323,13 @@ END
 {
 
 let pr_ltac_use_default b =
-  if b then (* Bug: a space is inserted before "..." *) str ".." else mt ()
+  if b.CAst.v then (* Bug: a space is inserted before "..." *) str ".." else mt ()
 
 }
 
 VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default }
-| [ "." ] -> { false }
-| [ "..." ] -> { true }
+| [ "." ] -> { CAst.make ~loc false }
+| [ "..." ] -> { CAst.make ~loc true }
 END
 
 {
@@ -364,15 +364,15 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
 END
 
 VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
-| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
+| [ "par" ":" ltac_info_opt(info) tactic(t) "." ] =>
     {
       let solving_tac = is_explicit_terminator t in
       let pbr = if solving_tac then Some "par" else None in
       VtProofStep{ proof_block_detection = pbr }
     } -> {
       let t, abstract = rm_abstract t in
       let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in
-      ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
+      ComTactic.solve_parallel ~info t ~abstract
     }
 END
 

plugins/ltac/g_ltac.mli

@@ -35,9 +35,9 @@ val wit_ltac_info : int Genarg.vernac_genarg_type
 
 val ltac_info : int Procq.Entry.t
 
-val wit_ltac_use_default : bool Genarg.vernac_genarg_type
+val wit_ltac_use_default : bool CAst.t Genarg.vernac_genarg_type
 
-val ltac_use_default : bool Procq.Entry.t
+val ltac_use_default : bool CAst.t Procq.Entry.t
 
 val wit_ltac_tactic_level : int Genarg.vernac_genarg_type
 

plugins/ltac2/g_ltac2.mlg

@@ -1049,7 +1049,7 @@ let toplevel_selector = G_vernac.toplevel_selector
 let pr_ltac2_selector s = Pp.(Goal_select.pr_goal_selector s ++ str ":")
 
 let pr_ltac2_use_default b =
-  if b then (* Bug: a space is inserted before "..." *) str ".." else mt ()
+  if b.CAst.v then (* Bug: a space is inserted before "..." *) str ".." else mt ()
 
 let subprf = G_vernac.subprf
 let subprf_with_selector = G_vernac.subprf_with_selector
@@ -1061,18 +1061,18 @@ VERNAC ARGUMENT EXTEND ltac2_selector PRINTED BY { pr_ltac2_selector }
 END
 
 VERNAC ARGUMENT EXTEND ltac2_use_default PRINTED BY { pr_ltac2_use_default }
-| [ "." ] -> { false }
-| [ "..." ] -> { true }
+| [ "." ] -> { CAst.make ~loc false }
+| [ "..." ] -> { CAst.make ~loc true }
 END
 
 VERNAC { tac2mode } EXTEND VernacLtac2
 | ![proof] [ ltac2_selector_opt(g) ltac2_expr(t) ltac2_use_default(with_end_tac) ] =>
   { classify_as_proofstep } -> { fun ~pstate ->
     Tac2entries.call ~pstate g ~with_end_tac t
   }
-| ![proof] [ "par" ":" ltac2_expr(t) ltac2_use_default(with_end_tac) ] =>
+| ![proof] [ "par" ":" ltac2_expr(t) "." ] =>
   { classify_as_proofstep } -> { fun ~pstate ->
-    Tac2entries.call_par ~pstate ~with_end_tac t
+    Tac2entries.call_par ~pstate t
   }
 END
 

plugins/ltac2/tac2entries.ml

@@ -1256,8 +1256,8 @@ let call ~pstate g ~with_end_tac tac =
   let g = Option.default (Goal_select.get_default_goal_selector()) g in
   ComTactic.solve ~pstate ~with_end_tac g ~info:None (ltac2_interp tac)
 
-let call_par ~pstate ~with_end_tac tac =
-  ComTactic.solve_parallel ~pstate ~info:None (ltac2_interp tac) ~abstract:false ~with_end_tac
+let call_par ~pstate tac =
+  ComTactic.solve_parallel ~pstate ~info:None (ltac2_interp tac) ~abstract:false
 
 (** Primitive algebraic types than can't be defined Rocq-side *)
 

plugins/ltac2/tac2entries.mli

@@ -70,11 +70,10 @@ val globalize_expr : raw_tacexpr -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Declare.Proof.t -> Goal_select.t option -> with_end_tac:bool -> raw_tacexpr
+val call : pstate:Declare.Proof.t -> Goal_select.t option -> with_end_tac:bool CAst.t -> raw_tacexpr
   -> Declare.Proof.t
 
-val call_par : pstate:Declare.Proof.t -> with_end_tac:bool -> raw_tacexpr
-  -> Declare.Proof.t
+val call_par : pstate:Declare.Proof.t -> raw_tacexpr -> Declare.Proof.t
 
 (** {5 Parsing entries} *)
 

stm/partac.ml

@@ -114,7 +114,7 @@ end = struct (* {{{ *)
             Declare.Proof.map pstate ~f:(Proof.focus focus_cond () r_goalno) in
           let pstate =
             ComTactic.solve ~pstate
-              Goal_select.SelectAll ~info:None tactic ~with_end_tac:false in
+              Goal_select.SelectAll ~info:None tactic ~with_end_tac:(CAst.make false) in
           let { Proof.sigma } = Declare.Proof.fold pstate ~f:Proof.data in
           let EvarInfo evi = Evd.find sigma r_goal in
           match Evd.(evar_body evi) with
@@ -190,7 +190,7 @@ let get_results res =
        spc () ++ prlist_with_sep spc int missing ++ str ")")
 
 let enable_par ~spawn_args ~nworkers = ComTactic.set_par_implementation
-  (fun ~pstate ~info t_ast ~abstract ~with_end_tac ->
+  (fun ~pstate ~info t_ast ~abstract ->
     let t_state = Vernacstate.freeze_full_state () in
     let t_state = Vernacstate.Stm.make_shallow t_state in
     TaskQueue.with_n_workers ~spawn_args nworkers CoqworkmgrApi.High (fun queue ->

stm/stm.ml

@@ -1934,7 +1934,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
            match (VCS.get_info base_state).state with
            | FullState { Vernacstate.interp = { lemmas } } ->
                Option.iter PG_compat.unfreeze lemmas;
-               PG_compat.with_current_proof (fun _ p ->
+               PG_compat.with_current_proof (fun p ->
                  feedback ~id:id Feedback.AddedAxiom;
                  fst (Proof.solve Goal_select.SelectAll None tac p), ());
                (* STATE SPEC:

theories/Corelib/Classes/CMorphisms.v

@@ -280,11 +280,11 @@ Section GenericInstances.
   Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H B R' H0 x y z X X0 x0 y0 X1.
     assert(R x0 x0).
-    - eapply transitivity with y0... now apply symmetry.
-    - eapply transitivity with (y x0)...
+    - eapply transitivity with y0; auto. now apply symmetry.
+    - eapply transitivity with (y x0); auto.
   Qed.
 
   Unset Strict Universe Declaration.
@@ -311,10 +311,10 @@ Section GenericInstances.
     `(Transitive A R) : Proper (R --> R ++> arrow) R.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x y X x0 y0 X0 X1.
-    apply transitivity with x...
-    apply transitivity with x0...
+    apply transitivity with x; auto.
+    apply transitivity with x0; auto.
   Qed.
 
   (** Proper declarations for partial applications. *)
@@ -324,51 +324,51 @@ Section GenericInstances.
   `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x x0 y X X0.
-    apply transitivity with y...
+    apply transitivity with y; auto.
   Qed.
 
   Global Program 
   Instance trans_co_impl_type_morphism
     `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x x0 y X X0.
-    apply transitivity with x0...
+    apply transitivity with x0; auto.
   Qed.
 
   Global Program 
   Instance trans_sym_co_inv_impl_type_morphism
     `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x x0 y X X0.
-    apply transitivity with y... apply symmetry...
+    apply transitivity with y; auto. apply symmetry; auto.
   Qed.
 
   Global Program Instance trans_sym_contra_arrow_morphism
     `(PER A R) {x} : Proper (R --> arrow) (R x) | 3.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x x0 y X X0.
-    apply transitivity with x0... apply symmetry...
+    apply transitivity with x0; auto. apply symmetry; auto.
   Qed.
 
   Global Program Instance per_partial_app_type_morphism
   `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x x0 y X.
     split.
-    - intros ; apply transitivity with x0...
+    - intros ; apply transitivity with x0; auto.
     - intros.
-      apply transitivity with y...
-      apply symmetry...
+      apply transitivity with y; auto.
+      apply symmetry; auto.
   Qed.
 
   (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
@@ -378,9 +378,9 @@ Section GenericInstances.
   `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x y X y0 y1 e X0; destruct e.
-    apply transitivity with y...
+    apply transitivity with y; auto.
   Qed.
 
   (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
@@ -389,14 +389,14 @@ Section GenericInstances.
   Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1.
 
   Next Obligation.
-  Proof with auto.
+  Proof.
     intros A R H x y X x0 y0 X0.
     split ; intros.
-    - apply transitivity with x0...
-      apply transitivity with x... apply symmetry...
+    - apply transitivity with x0; auto.
+      apply transitivity with x; auto. apply symmetry; auto.
 
-    - apply transitivity with y... apply transitivity with y0...
-      apply symmetry...
+    - apply transitivity with y; auto. apply transitivity with y0; auto.
+      apply symmetry; auto.
   Qed.
 
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).