aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Remove call to Refiner API from Funind.Pierre-Marie Pédrot
2020-05-07Port Evar_tactics to the new API.Pierre-Marie Pédrot
2020-05-07Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.Gaëtan Gilbert
2020-05-07Export API to recover values out of Ltac application.Pierre-Marie Pédrot
2020-05-07Add helper API to define low-level Ltac functions.Pierre-Marie Pédrot
2020-05-06Moving lazymatch and multimatch to simple identifiers.Hugo Herbelin
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
2020-05-06Documenting plugin/tactic/stdlib keywords in corresponding chapters.Hugo Herbelin
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
2020-05-05[ssr] wrap a couple of exception with tclLIFTEnrico Tassi
2020-05-04[ssr] get rid of (pf_)mkSsrConstEnrico Tassi
2020-05-04nit: don't open Persistent_cache in micromegaGaëtan Gilbert
2020-05-03[declare] Add deprecation notices for compat modules.Emilio Jesus Gallego Arias
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
2020-05-03[funind] Make `build_functional_principle` use a functional evar_mapEmilio Jesus Gallego Arias
2020-05-03Further port of ssr tacticsPierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Remove legacy API in SSR.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tacticsPierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further SSR port.Pierre-Marie Pédrot
2020-05-03Remove legacy SSR API.Pierre-Marie Pédrot
2020-05-03Further SSR port.Pierre-Marie Pédrot
2020-05-03Remove legacy layer in SSR.Pierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR code.Pierre-Marie Pédrot
2020-05-03Export new combinators in SSR not relying on the legacy API.Pierre-Marie Pédrot
2020-05-03Further porting of ssrcode.Pierre-Marie Pédrot
2020-05-03Slightly more tricky port of the ssr tactics.Pierre-Marie Pédrot
2020-05-03Further port SSReflect tactics to the new engine.Pierre-Marie Pédrot
2020-05-03Wrap ssr tactics into V82.tactic.Pierre-Marie Pédrot
2020-05-03Wrap a monadic combinator in a try-with block to catch exceptions.Pierre-Marie Pédrot
2020-05-03Remove a call to V82.tactic in Btauto.Pierre-Marie Pédrot
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
2020-05-02Move tclWRAPFINALLY to profile_ltacJason Gross
2020-05-02Decrease LtacProf overhead when not profilingJason Gross
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-05-01Warn when a (co)fixpoint is not truly recursive.Hugo Herbelin
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 17:22:06 +0000