aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/language/extensions/match.rst6
-rw-r--r--doc/sphinx/proof-engine/ltac.rst23
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst4
-rw-r--r--doc/sphinx/proof-engine/tactics.rst24
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--proofs/clenv.ml6
-rw-r--r--proofs/clenv.mli7
-rw-r--r--tactics/tactics.ml7
-rw-r--r--test-suite/bugs/closed/bug_12930.v10
-rw-r--r--test-suite/bugs/closed/bug_12944.v12
-rw-r--r--test-suite/success/induct.v10
-rw-r--r--vernac/proof_using.ml23
12 files changed, 90 insertions, 44 deletions
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 34752a4c4d..182f599a29 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -880,10 +880,10 @@ Here is a summary of the error messages corresponding to each
situation:
.. exn:: The constructor @ident expects @num arguments.
+ The variable ident is bound several times in pattern term
+ Found a constructor of inductive type term while a constructor of term is expected
- The variable ident is bound several times in pattern termFound a constructor
- of inductive type term while a constructor of term is expectedPatterns are
- incorrect (because constructors are not applied to the correct number of the
+ Patterns are incorrect (because constructors are not applied to the correct number of
arguments, because they are not linear or they are wrongly typed).
.. exn:: Non exhaustive pattern matching.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index e7ba82fb31..d8b2af092f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -375,8 +375,14 @@ behavior.)
| !
| par
- Applies :token:`ltac_expr` to the selected goals. It can only be used at the top
- level of a tactic expression; it cannot be used within a tactic expression.
+ Reorders the goals and applies :token:`ltac_expr` to the selected goals. It can
+ only be used at the top level of a tactic expression; it cannot be used within a
+ tactic expression. The selected goals are reordered so they appear after the
+ lowest-numbered selected goal, ordered by goal number. :ref:`Example
+ <reordering_goals_ex>`. If the selector applies
+ to a single goal or to all goals, the reordering will not be apparent. The order of
+ the goals in the :token:`selector` is irrelevant. (This may not be what you expect;
+ see `#8481 <https://github.com/coq/coq/issues/8481>`_.)
.. todo why shouldn't "all" and "!" be accepted anywhere a @selector is accepted?
It would be simpler to explain.
@@ -430,6 +436,19 @@ Selectors can also be used nested within a tactic expression with the
:name: No such goal. (Goal selector)
:undocumented:
+.. _reordering_goals_ex:
+
+.. example:: Selector reordering goals
+
+ .. coqtop:: reset in
+
+ Goal 1=0 /\ 2=0 /\ 3=0.
+
+ .. coqtop:: all
+
+ repeat split.
+ 1,3: idtac.
+
.. TODO change error message index entry
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 4480b10319..55e4f26fe8 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -156,6 +156,10 @@ list of assertion commands is given in :ref:`Assertions`. The command
``T``, then the commands ``Proof using a`` and ``Proof using T a``
are equivalent.
+ The set of declared variables always includes the variables used by
+ the statement. In other words ``Proof using e`` is equivalent to
+ ``Proof using Type + e`` for any declaration expression ``e``.
+
.. cmdv:: Proof using {+ @ident } with @tactic
Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index cff3f95804..2211a58e6e 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -54,7 +54,7 @@ Invocation of tactics
~~~~~~~~~~~~~~~~~~~~~
A tactic is applied as an ordinary command. It may be preceded by a
-goal selector (see Section :ref:`ltac-semantics`). If no selector is
+goal selector (see Section :ref:`goal-selectors`). If no selector is
specified, the default selector is used.
.. _tactic_invocation_grammar:
@@ -4744,9 +4744,13 @@ Non-logical tactics
.. tacn:: cycle @num
:name: cycle
- This tactic puts the :n:`@num` first goals at the end of the list of goals.
- If :n:`@num` is negative, it will put the last :math:`|num|` goals at the
+ Reorders the selected goals so that the first :n:`@num` goals appear after the
+ other selected goals.
+ If :n:`@num` is negative, it puts the last :n:`@num` goals at the
beginning of the list.
+ The tactic is only useful with a goal selector, most commonly `all:`.
+ Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent
+ to `all: cycle 1`. See :tacn:`… : … (goal selector)`.
.. example::
@@ -4764,10 +4768,12 @@ Non-logical tactics
.. tacn:: swap @num @num
:name: swap
- This tactic switches the position of the goals of indices :n:`@num` and
- :n:`@num`. Negative values for:n:`@num` indicate counting goals
- backward from the end of the focused goal list. Goals are indexed from 1,
- there is no goal with position 0.
+ Exchanges the position of the specified goals.
+ Negative values for :n:`@num` indicate counting goals
+ backward from the end of the list of selected goals. Goals are indexed from 1.
+ The tactic is only useful with a goal selector, most commonly `all:`.
+ Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent
+ to `all: swap 1 3`. See :tacn:`… : … (goal selector)`.
.. example::
@@ -4781,7 +4787,9 @@ Non-logical tactics
.. tacn:: revgoals
:name: revgoals
- This tactics reverses the list of the focused goals.
+ Reverses the order of the selected goals. The tactic is only useful with a goal
+ selector, most commonly `all :`. Note that other selectors reorder goals;
+ `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`.
.. example::
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6233807016..f69fe064a7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s =
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
| TacChange (check,op,c,h) ->
- let name = if check then "change_no_check" else "change" in
+ let name = if check then "change" else "change_no_check" in
hov 1 (
primitive name ++ brk (1,1)
++ (
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4893758ab3..31bc698830 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -713,12 +713,6 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
-let make_clenv_binding_env_apply env sigma n =
- make_clenv_binding_gen true n env sigma
-
-let make_clenv_binding_env env sigma =
- make_clenv_binding_gen false None env sigma
-
let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index d4905de434..a72c8c5e1f 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -75,17 +75,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
(** the arity of the lemma is fixed
the optional int tells how many prods of the lemma have to be used
use all of them if None *)
-val make_clenv_binding_env_apply :
- env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
- clausenv
-
val make_clenv_binding_apply :
env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
clausenv
-val make_clenv_binding_env :
- env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
-
val make_clenv_binding :
env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5f7e35d205..d33f3a5062 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3248,13 +3248,10 @@ let rec consume_pattern avoid na isdep gl = let open CAst in function
| {loc;v=IntroForthcoming true}::names when not isdep ->
consume_pattern avoid na isdep gl names
| {loc;v=IntroForthcoming _}::names as fullpat ->
- let avoid = Id.Set.union avoid (explicit_intro_names names) in
(CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat)
| {loc;v=IntroNaming IntroAnonymous}::names ->
- let avoid = Id.Set.union avoid (explicit_intro_names names) in
(CAst.make ?loc @@ intropattern_of_name gl avoid na, names)
| {loc;v=IntroNaming (IntroFresh id')}::names ->
- let avoid = Id.Set.union avoid (explicit_intro_names names) in
(CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names)
| pat::names -> (pat,names)
@@ -3312,7 +3309,7 @@ let get_recarg_dest (recargdests,tophyp) =
*)
let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
- let avoid = Id.Set.union avoid avoid' in
+ let avoid = Id.Set.union avoid' (Id.Set.union avoid (explicit_intro_names names)) in
let rec peel_tac ra dests names thin =
match ra with
| (RecArg,_,deprec,recvarname) ::
@@ -3320,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
Proofview.Goal.enter begin fun gl ->
let (recpat,names) = match names with
| [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] ->
- let id' = next_ident_away (add_prefix "IH" id) avoid in
+ let id' = new_fresh_id avoid (add_prefix "IH" id) gl in
(pat, [CAst.make @@ IntroNaming (IntroIdentifier id')])
| _ -> consume_pattern avoid (Name recvarname) deprec gl names in
let dest = get_recarg_dest dests in
diff --git a/test-suite/bugs/closed/bug_12930.v b/test-suite/bugs/closed/bug_12930.v
new file mode 100644
index 0000000000..e2a524301a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12930.v
@@ -0,0 +1,10 @@
+Section S.
+ Variable v : Prop.
+ Variable vv : v.
+ Collection easy := Type*.
+
+ Lemma ybar : v.
+ Proof using easy.
+ exact vv.
+ Qed.
+End S.
diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v
new file mode 100644
index 0000000000..d6720d9906
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12944.v
@@ -0,0 +1,12 @@
+
+Inductive vector A : nat -> Type :=
+ |nil : vector A 0
+ |cons : forall (h:A) (n:nat), vector A n -> vector A (S n).
+
+Global Set Mangle Names.
+
+Lemma vlookup_middle {A n} (v : vector A n) : True.
+Proof.
+ induction v as [|?? IHv].
+ all:exact I.
+Qed.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 73fe53c757..a39b17e1f1 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -196,3 +196,13 @@ Goal forall m n:nat, n=m.
double induction m n.
Abort.
+(* Mentioned as part of bug #12944 *)
+
+Inductive test : Set := cons : forall (IHv : nat) (v : test), test.
+
+Goal test -> test.
+induction 1 as [? IHv].
+Undo.
+destruct 1 as [? IHv].
+exact IHv. (* Check that the name is granted *)
+Qed.
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 2130a398e9..95680c2a4e 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -41,28 +41,27 @@ let set_of_type env ty =
let full_set env =
List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
-let rec process_expr env e ty =
+let process_expr env e v_ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
- | SsType -> set_of_type env ty
- | SsSingl { CAst.v = id } -> set_of_id env id
+ | SsType -> v_ty
+ | SsSingl { CAst.v = id } -> set_of_id id
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
| SsFwdClose e -> close_fwd env (aux e)
+ and set_of_id id =
+ if Id.to_string id = "All" then
+ full_set env
+ else if CList.mem_assoc_f Id.equal id !known_names then
+ aux (CList.assoc_f Id.equal id !known_names)
+ else Id.Set.singleton id
in
- aux e
-
-and set_of_id env id =
- if Id.to_string id = "All" then
- List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
- else if CList.mem_assoc_f Id.equal id !known_names then
- process_expr env (CList.assoc_f Id.equal id !known_names) []
- else Id.Set.singleton id
+ aux e
let process_expr env e ty =
let v_ty = set_of_type env ty in
- let s = Id.Set.union v_ty (process_expr env e ty) in
+ let s = Id.Set.union v_ty (process_expr env e v_ty) in
Id.Set.elements s
let name_set id expr = known_names := (id,expr) :: !known_names
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:20:23 +0000