aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
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-20Merge PR #13721: Remove strong reduction wrapperscoqbot-app[bot]
Reviewed-by: mattam82
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-18Preventing internal temporary names to impact the "?H"-like intro-pattern names.Hugo Herbelin
2021-01-18Further simplifications in intro_patterns machinery.Hugo Herbelin
2021-01-18Small reworking of code in intros-pattern.Hugo Herbelin
We compute earlier if "apply in" clears or not. We inline prepare_naming into its only client prepare_intros_opt (using the more general make_naming instead).
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
We build earlier the final expected name at the end of a sequence of "%" introduction patterns.
2021-01-18Move the two only calls to the strong combinator to their calling site.Pierre-Marie Pédrot
2021-01-18Move the only use of strong_with_flags to its single calling module.Pierre-Marie Pédrot
This also allows to move the strong variant of cbn to the Cbn module.
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-11Use the Evarutil cache for Class_tactics.evar_dependencies.Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
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.
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 #13628: Cache meta instances in Clenvcoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: gares Ack-by: SkySkimmer
2020-12-15Merge PR #13609: Extrude the computation of redexp flags in reduce.coqbot-app[bot]
Reviewed-by: herbelin
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-12-13Removing unused internal introduction-patterns flag assert_style.Hugo Herbelin
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-12Small API encapsulation inside Redexpr.Pierre-Marie Pédrot
We move bind_red_expr_occurrences from Tactics to Redexpr, where it semantically belongs. We also hide it and seal the corresponding evaluated types.
2020-12-12Extrude the computation of redexp flags in reduce.Pierre-Marie Pédrot
This was a source of slowdown observed in bedrock2.
2020-12-12Split the intepretation of red_exprs in two phases.Pierre-Marie Pédrot
2020-12-12Generalize the type of red_expr w.r.t. the type of flags they contain.Pierre-Marie Pédrot
2020-12-02Stop calling Id.Map.domain on univ binders every individual universeGaëtan Gilbert
2020-11-28Merge PR #13502: A small fix for freshness in the `change` tacticcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
Reviewed-by: gares
2020-11-27A small fix for freshness in the `change` tacticJasper Hugunin
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to ↵Pierre-Marie Pédrot
check resolution of evars more incrementally Ack-by: SkySkimmer Reviewed-by: gares Ack-by: ppedrot
2020-11-26Fixes #13456: regression where tactic exists started to check evars ↵Hugo Herbelin
incrementally. The regression was due to #12365. We fix it by postponing the evars check after the calls to the underlying constructor tactic, while retaining using information from the first instantiations to resolve the latter instantiations.
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-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
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-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ↵Pierre-Marie Pédrot
naming Ack-by: gares Reviewed-by: ppedrot
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
Also some dead code. If no typo is introduced, there should be no semantic changes.
2020-11-04Do not try to be clever for term-as-hint interpretation.Pierre-Marie Pédrot
The prepare_hint function was trying to requantify over all undefined evars, but actually this should not happen when defining generic terms as hints through some Hint vernacular command.
2020-11-04Opacify the Hints.hint_term type.Pierre-Marie Pédrot
2020-11-04Encapsulate the last use of IsConstr in the Hints API.Pierre-Marie Pédrot
2020-11-04Further API cleanup after the removal of forward hints.Pierre-Marie Pédrot
We know statically that only global references are passed to make_resolves.
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
This is similar to Constant and MutInd but for some reason this was was never done. Such a patch makes the whole API more regular. We also deprecate the legacy aliases.
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 10:53:32 +0000