aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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]
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
2020-11-27A small fix for freshness in the `change` tacticJasper Hugunin
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-11-27Merge PR #13468: Fixes #13456: regression in tactic exists which started to c...Pierre-Marie Pédrot
2020-11-26Fixes #13456: regression where tactic exists started to check evars increment...Hugo Herbelin
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
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]
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
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
2020-11-04Do not try to be clever for term-as-hint interpretation.Pierre-Marie Pédrot
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
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
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-29Adding a few tacticals for the purpose of porting funind to new proof engine.Hugo Herbelin
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ...coqbot-app[bot]
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-18Remove unused API from Dn.Pierre-Marie Pédrot
2020-09-18Clean up a bit the implemenation of dnets.Pierre-Marie Pédrot
2020-09-18Remove dead code in dnets.Pierre-Marie Pédrot
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo Herbelin
2020-09-13Statically ensure that only polymophic hint terms come with a context.Pierre-Marie Pédrot
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
2020-09-10Add a fast-path to Tactics.e_change_in_hyps.Pierre-Marie Pédrot
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment...Pierre-Marie Pédrot
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-06Merge PR #12976: Remove clenv chaining in EqualityHugo Herbelin
2020-09-04Remove the last use of clenv_fchain in Equality.Pierre-Marie Pédrot
2020-09-04Inline the last use of apply_on_clause in Equality.Pierre-Marie Pédrot
2020-09-04Remove a useless use of clenv_fchain in Equality.Pierre-Marie Pédrot
2020-09-04Statically enforce that elim is passed a fully applied inductive type.Pierre-Marie Pédrot
2020-09-04Restrict a spurious call to a reduction to a quantified inductive type.Pierre-Marie Pédrot
2020-09-04Defunctionalize the mk_elim creation in Elim.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:04:14 +0000