aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-24added numeral_notation to META.coq.inAli Caglayan
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its declar...Maxime Dénès
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to be...Pierre-Marie Pédrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
2020-08-19Prefer eval_tactic_ist, which has error localisation, to interp_tactic.Hugo Herbelin
2020-08-19In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API.Hugo Herbelin
2020-08-19Merge PR #12856: Adding a mention of the JSON extraction in the documentation.coqbot
2020-08-19Merge PR #12709: Simplify hint pattern handlingMatthieu Sozeau
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-19Add overlay.Pierre-Marie Pédrot
2020-08-19Replace Hints.head_constr_bound with Hints.head_bound.Pierre-Marie Pédrot
2020-08-19Simplify the computation of the head global for hint patterns.Pierre-Marie Pédrot
2020-08-19Ensure statically that Hint Extern comes with a pattern.Pierre-Marie Pédrot
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
2020-08-19Merge PR #12822: Do not precompute hint dnets eagerlyMatthieu Sozeau
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-19Merge PR #12774: Fixing tactic loc updating in #12223Pierre-Marie Pédrot
2020-08-18Extraction: At declaration point of a global, use its declaring name.Hugo Herbelin
2020-08-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 15:19:31 +0000