aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-18Tactic replace: adding support for registration of an equality in Type.Hugo Herbelin
2020-08-18Tactic inversion: adding support for registration of an equality in Type.Hugo Herbelin
2020-08-17Merge PR #12841: Recommend replace as a replacement to cutrewrite.coqbot
2020-08-17Merge PR #12802: Document semantic restriction on patterns in Gallina match c...coqbot
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
2020-08-17Merge PR #12751: Fixes reduction effect printing in the presence of non purel...Pierre-Marie Pédrot
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-08-14Do not precompute hint dnets eagerly.Pierre-Marie Pédrot
2020-08-13Merge PR #12823: Move reduce_mind_case from Reductionops to Tacred.Enrico Tassi
2020-08-13Merge PR #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
2020-08-13Merge PR #12720: Factor code related to class hint clenvHugo Herbelin
2020-08-13Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets.Hugo Herbelin
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
2020-08-13Merge PR #12479: Bring Int63 notations into line with stdlibAnton Trunov
2020-08-12Merge PR #12748: Windows CI: changed cygwin repo servercoqbot
2020-08-12Add overlays.Pierre-Marie Pédrot
2020-08-12Cosmetic changes as suggested by SkySkimmer.Pierre-Marie Pédrot
2020-08-12Further code simplification in typeclass resolution tactic.Pierre-Marie Pédrot
2020-08-12Split the uses of connect_hint_clenv into two different functions.Pierre-Marie Pédrot
2020-08-12Remove dead code after the previous commit.Pierre-Marie Pédrot
2020-08-12Tentatively more efficient implementation of e_give_exact for typeclasses.Pierre-Marie Pédrot
2020-08-12Export a dedicated function that applies immediately a hint.Pierre-Marie Pédrot
2020-08-12Code simplification around hint manipulation in Class_tactics.Pierre-Marie Pédrot
2020-08-12Make the Hint.hint type private.Pierre-Marie Pédrot
2020-08-12Move connect_hint_clenv from Auto to Hints.Pierre-Marie Pédrot
2020-08-12Do not do a round trip with auto hint representation in autoapply.Pierre-Marie Pédrot
2020-08-12Do not tamper with hints in Class_tactics.with_prods.Pierre-Marie Pédrot
2020-08-12Perfom an goal enter in the relevant class tactics instead of outside.Pierre-Marie Pédrot
2020-08-12Inline Class_tactics.clenv_of_prods.Pierre-Marie Pédrot
2020-08-12Additional statements about List.repeatOlivier Laurent
2020-08-12Windows CI: changed cygwin repo serverMichael Soegtrop
2020-08-11add deprecation to changelogYishuai Li
2020-08-11deprecate prod_curry and prod_uncurryYishuai Li
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
2020-08-11Small code simplification in contract_(co)fix.Pierre-Marie Pédrot
2020-08-11Move reduce_mind_case from Reductionops to Tacred.Pierre-Marie Pédrot
2020-08-11Merge PR #12794: Repair coqide option "Display parentheses"Pierre-Marie Pédrot
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
2020-08-10[micromega] Fix bug#12790Frédéric Besson
2020-08-10[zify] fix for bug#12791Frédéric Besson
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-09Bring Int63 notations into line with stdlibJason Gross
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-08-09Fixing a coercion entry transitivity bug.Hugo Herbelin
2020-08-08Merge PR #12796: [default.nix] Propagate dependency on num following #12604.Vincent Laporte
2020-08-07[default.nix] Propagate dependency on num following #12604.Théo Zimmermann
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environm...coqbot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 02:59:36 +0000