aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
2020-12-15Merge PR #13609: Extrude the computation of redexp flags in reduce.coqbot-app[bot]
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
2020-12-12Extrude the computation of redexp flags in reduce.Pierre-Marie Pédrot
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]
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:48:35 +0000