aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Port Evar_tactics to the new API.Pierre-Marie Pédrot
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-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-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
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-04-02Merge PR #12002: Cleanup tactic_option a bitPierre-Marie Pédrot
2020-04-02Cleanup tactic_option a bitGaëtan Gilbert
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-31[declare] [rewrite] Use high-level declare API, part II.Emilio Jesus Gallego Arias
2020-03-31[declare] [rewrite] Use high-level declare API, part I.Emilio Jesus Gallego Arias
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-08Merge PR #11578: [exn] Keep information from multiple extra exn handlersPierre-Marie Pédrot
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
2020-03-04Merge PR #11709: Deprecate the "prolog" tactic.Théo Zimmermann
2020-03-03[exn] Keep information from multiple extra exn handlersEmilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:25:31 +0000