aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/04-tactics/12423-rm-info.rst2
-rw-r--r--doc/changelog/10-standard-library/12484-fix12483.rst6
-rw-r--r--doc/sphinx/changes.rst24
-rw-r--r--plugins/ltac/g_ltac.mlg3
-rw-r--r--plugins/ltac/pptactic.ml6
-rw-r--r--plugins/ltac/tacexpr.ml1
-rw-r--r--plugins/ltac/tacexpr.mli1
-rw-r--r--plugins/ltac/tacintern.ml1
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tacsubst.ml1
-rw-r--r--tactics/tactics.ml59
-rw-r--r--test-suite/modules/PO.v10
-rw-r--r--test-suite/output/auto.v2
-rw-r--r--test-suite/output/bug12442.out6
-rw-r--r--test-suite/output/bug12442.v10
15 files changed, 77 insertions, 65 deletions
diff --git a/doc/changelog/04-tactics/12423-rm-info.rst b/doc/changelog/04-tactics/12423-rm-info.rst
new file mode 100644
index 0000000000..bf20453e6b
--- /dev/null
+++ b/doc/changelog/04-tactics/12423-rm-info.rst
@@ -0,0 +1,2 @@
+- **Removed:** Removed info tactic that was deprecated in 8.5.
+ (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle).
diff --git a/doc/changelog/10-standard-library/12484-fix12483.rst b/doc/changelog/10-standard-library/12484-fix12483.rst
deleted file mode 100644
index 95e7c150a3..0000000000
--- a/doc/changelog/10-standard-library/12484-fix12483.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
- Fix the specification of :n:`PrimFloat.leb` which made
- :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`.
- (`#12484 <https://github.com/coq/coq/pull/12484>`_,
- fixes `#12483 <https://github.com/coq/coq/issues/12483>`_,
- by Pierre Roux).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 51c80e697e..8427300dc4 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -96,6 +96,16 @@ Changes in 8.12+beta1
.. contents::
:local:
+Kernel
+^^^^^^
+
+- **Fixed:**
+ Specification of :n:`PrimFloat.leb` which made
+ :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`.
+ (`#12484 <https://github.com/coq/coq/pull/12484>`_,
+ fixes `#12483 <https://github.com/coq/coq/issues/12483>`_,
+ by Pierre Roux).
+
Specification language, type inference
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -1040,8 +1050,9 @@ Reference manual
`#11423 <https://github.com/coq/coq/pull/11423>`_,
`#11705 <https://github.com/coq/coq/pull/11705>`_,
`#11718 <https://github.com/coq/coq/pull/11718>`_,
- `#11720 <https://github.com/coq/coq/pull/11720>`_
- and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim
+ `#11720 <https://github.com/coq/coq/pull/11720>`_,
+ `#11961 <https://github.com/coq/coq/pull/11961>`_
+ and `#12103 <https://github.com/coq/coq/pull/12103>`_, by Jim
Fehrle, reviewed by Théo Zimmermann).
- **Added:**
A glossary of terms and an index of attributes
@@ -1068,10 +1079,11 @@ Reference manual
`#11720 <https://github.com/coq/coq/pull/11720>`_
`#11797 <https://github.com/coq/coq/pull/11797>`_,
`#11913 <https://github.com/coq/coq/pull/11913>`_,
- `#11958 <https://github.com/coq/coq/pull/11958>`_
- `#11960 <https://github.com/coq/coq/pull/11960>`_
- and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim
- Fehrle, reviewed by Théo Zimmermann).
+ `#11958 <https://github.com/coq/coq/pull/11958>`_,
+ `#11960 <https://github.com/coq/coq/pull/11960>`_,
+ `#11961 <https://github.com/coq/coq/pull/11961>`_
+ and `#12103 <https://github.com/coq/coq/pull/12103>`_, by Jim
+ Fehrle, reviewed by Théo Zimmermann and Jason Gross).
Infrastructure and dependencies
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 0e661543db..996f6b3eb3 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -173,8 +173,7 @@ GRAMMAR EXTEND Gram
{ TacFun (it,body) }
| "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
llc = LIST1 let_clause SEP "with"; "in";
- body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) }
- | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ]
+ body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
;
(* Tactic arguments to the right of an application *)
tactic_arg_compat:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d74e981c6d..6233807016 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -642,7 +642,6 @@ let pr_goal_selector ~toplevel s =
let lcall = 1
let leval = 1
let ltatom = 1
- let linfo = 5
let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq
@@ -988,11 +987,6 @@ let pr_goal_selector ~toplevel s =
keyword "infoH" ++ spc ()
++ pr_tac (LevelLe ltactical) t),
ltactical
- | TacInfo t ->
- hov 1 (
- keyword "info" ++ spc ()
- ++ pr_tac (LevelLe ltactical) t),
- linfo
| TacOr (t1,t2) ->
hov 1 (
pr_tac (LevelLt lorelse) t1 ++ spc ()
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index b77fb3acc7..b261096b63 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -225,7 +225,6 @@ and 'a gen_tactic_expr =
'a gen_tactic_expr * Id.t option
| TacId of 'n message_token list
| TacFail of global_flag * int or_var * 'n message_token list
- | TacInfo of 'a gen_tactic_expr
| TacLetIn of rec_flag *
(lname * 'a gen_tactic_arg) list *
'a gen_tactic_expr
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index cfa224319c..650349b586 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -224,7 +224,6 @@ and 'a gen_tactic_expr =
'a gen_tactic_expr * Id.t option
| TacId of 'n message_token list
| TacFail of global_flag * int or_var * 'n message_token list
- | TacInfo of 'a gen_tactic_expr
| TacLetIn of rec_flag *
(lname * 'a gen_tactic_arg) list *
'a gen_tactic_expr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index bcfdb5318e..afa79a88db 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -649,7 +649,6 @@ and intern_tactic_seq onlytac ist = function
| TacDo (n,tac) ->
ist.ltacvars, TacDo (intern_int_or_var ist n,intern_pure_tactic ist tac)
| TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac)
- | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac)
| TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
| TacTimeout (n,tac) ->
ist.ltacvars, TacTimeout (intern_int_or_var ist n,intern_tactic onlytac ist tac)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 97f7a198e6..705a1a62ce 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1035,13 +1035,6 @@ let type_uconstr ?(flags = (constr_flags ()))
understand_ltac flags env sigma vars expected_type term
end
-let warn_deprecated_info =
- CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
- (fun () ->
- strbrk "The general \"info\" tactic is currently not working." ++ spc()++
- strbrk "There is an \"Info\" command to replace it." ++fnl () ++
- strbrk "Some specific verbose tactics may also exist, such as info_eauto.")
-
(* Interprets an l-tac expression into a value *)
let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =
(* The name [appl] of applied top-level Ltac names is ignored in
@@ -1154,9 +1147,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
| TacArg a -> interp_tactic ist (TacArg a)
- | TacInfo tac ->
- warn_deprecated_info ();
- eval_tactic ist tac
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index ed298b7e66..c2f1589b74 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -200,7 +200,6 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
| TacTime (s,tac) -> TacTime (s,subst_tactic subst tac)
| TacTry tac -> TacTry (subst_tactic subst tac)
- | TacInfo tac -> TacInfo (subst_tactic subst tac)
| TacRepeat tac -> TacRepeat (subst_tactic subst tac)
| TacOr (tac1,tac2) ->
TacOr (subst_tactic subst tac1,subst_tactic subst tac2)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 315c42097d..65f79b6a51 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -490,12 +490,18 @@ let assert_before_gen b naming t =
let assert_before na = assert_before_gen false (naming_of_name na)
let assert_before_replacing id = assert_before_gen true (NamingMustBe (CAst.make id))
-let assert_after_then_gen b naming t tac =
+let replace_error_option err tac =
+ match err with
+ | None -> tac
+ | Some (e, info) ->
+ Proofview.tclORELSE tac (fun _ -> Proofview.tclZERO ~info e)
+
+let assert_after_then_gen ?err b naming t tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in
Tacticals.New.tclTHENFIRST
- (internal_cut_rev b id t)
+ (replace_error_option err (internal_cut_rev b id t))
(tac id)
end
@@ -1366,7 +1372,7 @@ let do_replace id = function
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
-let clenv_refine_in with_evars targetid id sigma0 clenv tac =
+let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
{ clenv with evd = Typeclasses.resolve_typeclasses
@@ -1383,7 +1389,7 @@ let clenv_refine_in with_evars targetid id sigma0 clenv tac =
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
(Tacticals.New.tclTHENLAST
- (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
+ (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)
(********************************************)
(* Elimination tactics *)
@@ -1668,24 +1674,28 @@ let descend_in_conjunctions avoid tac (err, info) c =
let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
let elim = EConstr.of_constr elim in
NotADefinedRecordUseScheme elim in
- Tacticals.New.tclORELSE0
- (Tacticals.New.tclFIRST
- (List.init n (fun i ->
+ let or_tac t1 t2 e = Proofview.tclORELSE (t1 e) t2 in
+ List.fold_right or_tac
+ (List.init n (fun i (err, info) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
match make_projection env sigma params cstr sign elim i n c u with
| None ->
- let info = Exninfo.reify () in
- Tacticals.New.tclFAIL ~info 0 (mt())
+ Proofview.tclZERO ~info err
| Some (p,pt) ->
Tacticals.New.tclTHENS
- (assert_before_gen false (NamingAvoid avoid) pt)
- [refiner ~check:true EConstr.Unsafe.(to_constr p);
+ (Proofview.tclORELSE
+ (assert_before_gen false (NamingAvoid avoid) pt)
+ (fun _ -> Proofview.tclZERO ~info err))
+ [Proofview.tclORELSE
+ (refiner ~check:true EConstr.Unsafe.(to_constr p))
+ (fun _ -> Proofview.tclZERO ~info err);
(* Might be ill-typed due to forbidden elimination. *)
- Tacticals.New.onLastHypId (tac (not isrec))]
- end)))
- (Proofview.tclZERO ~info err)
+ Tacticals.New.onLastHypId (tac (err, info) (not isrec))]
+ end))
+ (fun (err, info) -> Proofview.tclZERO ~info err)
+ (err, info)
| None -> Proofview.tclZERO ~info err
with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
end
@@ -1750,7 +1760,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
let tac =
if with_destruct then
descend_in_conjunctions Id.Set.empty
- (fun b id ->
+ (fun _ b id ->
Tacticals.New.tclTHEN
(try_main_apply b (mkVar id))
(clear [id]))
@@ -1879,7 +1889,7 @@ let apply_in_once ?(respect_opaque = false) with_delta
let t' = Tacmach.New.pf_get_hyp_typ id gl in
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in
- let rec aux idstoclear with_destruct c =
+ let rec aux ?err idstoclear with_destruct c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -1891,18 +1901,17 @@ let apply_in_once ?(respect_opaque = false) with_delta
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
- clenv_refine_in with_evars targetid id sigma clause
+ clenv_refine_in ?err with_evars targetid id sigma clause
(fun id ->
- Tacticals.New.tclTHENLIST [
- apply_clear_request clear_flag false c;
- clear idstoclear;
- tac id
- ])
+ replace_error_option err (
+ apply_clear_request clear_flag false c <*>
+ clear idstoclear) <*>
+ tac id)
with e when with_destruct && CErrors.noncritical e ->
- let (e, info) = Exninfo.capture e in
+ let err = Option.default (Exninfo.capture e) err in
(descend_in_conjunctions (Id.Set.singleton targetid)
- (fun b id -> aux (id::idstoclear) b (mkVar id))
- (e, info) c)
+ (fun err b id -> aux ~err (id::idstoclear) b (mkVar id))
+ err c)
end
in
aux [] with_destruct d
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 4c0ee1b5bd..767b3c1922 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -23,11 +23,11 @@ Module Pair (X: PO) (Y: PO) <: PO.
Hint Unfold le.
Lemma le_refl : forall p : T, le p p.
- info auto.
+ auto.
Qed.
Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
- unfold le; intuition; info eauto.
+ unfold le; intuition; eauto.
Qed.
Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
@@ -39,9 +39,9 @@ Module Pair (X: PO) (Y: PO) <: PO.
enough (t0 = t2) as ->.
reflexivity.
- info auto.
+ auto.
- info auto.
+ auto.
Qed.
End Pair.
@@ -53,5 +53,5 @@ Require Nat.
Module NN := Pair Nat Nat.
Lemma zz_min : forall p : NN.T, NN.le (0, 0) p.
- info auto with arith.
+ auto with arith.
Qed.
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
index 92917cdfc7..7b295dd1cb 100644
--- a/test-suite/output/auto.v
+++ b/test-suite/output/auto.v
@@ -1,4 +1,4 @@
-(* testing info/debug auto/eauto *)
+(* testing info_*/debug auto/eauto *)
Goal False \/ (True -> True).
info_auto.
diff --git a/test-suite/output/bug12442.out b/test-suite/output/bug12442.out
new file mode 100644
index 0000000000..644ef6cd7c
--- /dev/null
+++ b/test-suite/output/bug12442.out
@@ -0,0 +1,6 @@
+The command has indeed failed with message:
+No product even after head-reduction.
+The command has indeed failed with message:
+Not an inductive product.
+The command has indeed failed with message:
+Not an inductive product.
diff --git a/test-suite/output/bug12442.v b/test-suite/output/bug12442.v
new file mode 100644
index 0000000000..481989a4e9
--- /dev/null
+++ b/test-suite/output/bug12442.v
@@ -0,0 +1,10 @@
+Parameter A B : Prop.
+Axiom P : inhabited (A -> B).
+
+Goal A -> True.
+Proof.
+ Fail intros ?%P ?.
+ Fail intros []%P.
+ intro a.
+ Fail apply P in a as [].
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:56:37 +0000