aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-05-29Merge PR #12421: Fixes for compilation without native dynlinkEmilio Jesus Gallego Arias
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18[declare] Grand unification of the proof save path.Emilio Jesus Gallego Arias
2020-05-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
2020-05-16[micromega] Revert bad change from 5001deed21e8f4027411cc6413a9d2b98e1bcceeEmilio Jesus Gallego Arias
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Move SSR's Search to a new plugin and deprecate it.Théo Zimmermann
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-14Tweak the error message of reference internalization.Pierre-Marie Pédrot
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Merge PR #12214: nit: don't open Persistent_cache in micromegaVincent Laporte
2020-05-13Ssrmatching: Hack to circumvent a hack.Hugo Herbelin
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
2020-05-13Merge PR #12307: Cleaning up the legacy proof engineEmilio Jesus Gallego Arias
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
2020-05-12Remove useless try-with clauses in newring.Pierre-Marie Pédrot
2020-05-12Remove useless try-with blocks in congruence.Pierre-Marie Pédrot
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo Herbelin
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
2020-05-11Merge PR #12129: Add a `with_strategy` tacticPierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-10Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255).Hugo Herbelin
2020-05-09Merge PR #12241: [declare] Merge DeclareDef into DeclareGaëtan Gilbert
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Add hexadecimal numeralsPierre Roux
2020-05-09Rename functionsPierre Roux
2020-05-09Merge PR #12204: Ltac helper functions APIHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
2020-05-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:43:23 +0000