diff options
| -rw-r--r-- | CHANGES | 36 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh | 21 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/coretactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 26 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
7 files changed, 49 insertions, 50 deletions
@@ -7,6 +7,22 @@ Tactics Use with Set Default Goal Selector to force focusing before tactics are called. +- The undocumented "nameless" forms `fix N`, `cofix` that were + deprecated in 8.8 have been removed from LTAC's syntax; please use + `fix ident N/cofix ident` to explicitely name the (co)fixpoint + hypothesis to be introduced. + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + +- Support for fix/cofix added in Ltac "match" and "lazymatch". + +- Ltac backtraces now include trace information about tactics + called by OCaml-defined tactics. + +- Option "Ltac Debug" now applies also to terms built using Ltac functions. + Tools - Coq_makefile lets one override or extend the following variables from @@ -22,20 +38,6 @@ Vernacular Commands By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. -Tactics - -- Introduction tactics "intro"/"intros" on a goal which is an - existential variable now force a refinement of the goal into a - dependent product rather than failing. - -Tactic language - -- Support for fix/cofix added in Ltac "match" and "lazymatch". - -- Ltac backtraces now include trace information about tactics - called by OCaml-defined tactics. -- Option "Ltac Debug" now applies also to terms built using Ltac functions. - Coq binaries and process model - Before 8.9, Coq distributed a single `coqtop` binary and a set of @@ -67,9 +69,9 @@ Tools Tactic language -- The undocumented "nameless" forms `fix N`, `cofix N` have been - deprecated; please use `fix/cofix ident N` to explicitely name - hypothesis to be introduced. +- The undocumented "nameless" forms `fix N`, `cofix` have been + deprecated; please use `fix ident N /cofix ident` to explicitely + name the (co)fixpoint hypothesis to be introduced. Documentation diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh new file mode 100644 index 000000000..ea9cd8ee0 --- /dev/null +++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then + + # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 + # + # equations + # ltac2 + + # The below developments should instead use a backwards compatible fix. + # + # color + # iris-lambda-rust + # math-classes + # formal-topology + + ltac2_CI_BRANCH=tactics+push_fix_naming_out + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=tactics+push_fix_naming_out + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ccf109ce1..5e0d3e8ee 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1242,7 +1242,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1))) else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) @@ -1657,7 +1657,7 @@ let prove_principle_for_gen (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 45c9eff2f..ab03f1831 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1152,7 +1152,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 931633e1a..faa9e413b 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -273,15 +273,13 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Tactics.fix None n ] -| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] + [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Tactics.cofix None ] -| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] + [ "cofix" ident(id) ] -> [ Tactics.cofix id ] END (* Clear *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 01351e249..a42e4b44b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -563,20 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> end end -let warning_nameless_fix = - CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () -> - str "fix/cofix without a name are deprecated, please use the named version.") - -let fix ido n = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_fix id n [] 0 - end - | Some id -> - mutual_fix id n [] 0 +let fix id n = mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in @@ -619,16 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> end end -let cofix ido = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_cofix id [] 0 - end - | Some id -> - mutual_cofix id [] 0 +let cofix id = mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 46f782eaa..ddf78b1d4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -41,9 +41,9 @@ val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic -val fix : Id.t option -> int -> unit Proofview.tactic +val fix : Id.t -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic -val cofix : Id.t option -> unit Proofview.tactic +val cofix : Id.t -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic |