aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Collapse)Author
2021-01-28Merge PR #13790: [vernac] Check that no proofs do remain open at ↵coqbot-app[bot]
section/module closing time Reviewed-by: SkySkimmer
2021-01-27[ltac] break dependency on the STMEnrico Tassi
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
Fixes #13755 .
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel.
2020-12-18Merge PR #13530: Revert removal of eoi_entry in #13447coqbot-app[bot]
Reviewed-by: herbelin
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
We additionally check that occurrence 0 is invalid in simpl at, unfold at, etc.
2020-12-11Revert removal of eoi_entry in #13447Jim Fehrle
2020-12-11Use a registered printer for tactic coercion failure.Pierre-Marie Pédrot
Otherwise we pay a high cost for printing that might never make it to the user.
2020-11-29Merge PR #13510: Add missing print registration for wit_nat_or_varcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-29Fixing printing of apply in (continuation of #12246).Hugo Herbelin
2020-11-28Add missing print registration for wit_nat_or_varJim Fehrle
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
Reviewed-by: mattam82
2020-11-25Merge PR #13447: Remove unused parsing codecoqbot-app[bot]
Reviewed-by: herbelin
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
This allows proper treatment in notations, ie fixes #13303 The "glob" representation of universes (what pretyping sees) contains only fully interpreted (kernel) universes and unbound universe ids (for non Strict Universe Declaration). This means universes need to be understood at intern time, so intern now has a new "universe binders" argument. We cannot avoid this due to the following example: ~~~coq Module Import M. Universe i. End M. Definition foo@{i} := Type@{i}. ~~~ When interning `Type@{i}` we need to know that `i` is locally bound to avoid interning it as `M.i`. Extern has a symmetrical problem: ~~~coq Module Import M. Universe i. End M. Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. Print foo. (* must not print Type@{i} -> Type@{i} *) ~~~ (Polymorphic as otherwise the local `i` will be called `foo.i`) Therefore extern also takes a universe binders argument. Note that the current implementation actually replaces local universes with names at detype type. (Asymmetrical to pretyping which only gets names in glob terms for dynamically declared univs, although it's capable of understanding bound univs too) As such extern only really needs the domain of the universe binders (ie the set of bound universe ids), we just arbitrarily pass the whole universe binders to avoid putting `Id.Map.domain` at every entry point. Note that if we want to change so that detyping does not name locally bound univs we would need to pass the reverse universe binders (map from levels to ids, contained in the ustate ie in the evar map) to extern.
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-22Remove unused parsing codeJim Fehrle
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the ↵Pierre-Marie Pédrot
same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas ↵Pierre-Marie Pédrot
(hopefully) Reviewed-by: ppedrot
2020-11-18Merge PR #13251: Make sure that setoid_rewrite passes state to subgoalsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-17Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.Hugo Herbelin
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-16Suggesting to use injection when an injection pattern is given to destruct.Hugo Herbelin
This hopefully clarifies the confusing role of destruct (see #13205).
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
Fix #13246 Not sure if this is the right thing to do, but it seems to work.
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-12Revert to "using" not being a keyword in -noinit mode.Théo Zimmermann
The IDENT annotations in g_ltac.mlg are required to not break the parser.
2020-11-12Add support for Proof using in -noinit mode.Théo Zimmermann
"Proof with" is Ltac-specific but there is no reason why it should be the same for "Proof using".
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ↵Pierre-Marie Pédrot
on the inner calls Reviewed-by: ppedrot
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
Ltac variables were not yet supported.
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
Adopting the same format means printing "Ltac foo := ..." and not the fully qualified name of foo.
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the ↵Hugo Herbelin
inner calls). This continues #12223, #12773, #12992, #12774, #12999.
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: herbelin Ack-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 19:39:03 +0000