aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)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
Reviewed-by: Matafou Reviewed-by: SkySkimmer Reviewed-by: ppedrot
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
The real list is computed by tok_using in CLexer.
2020-05-06Documenting plugin/tactic/stdlib keywords in corresponding chapters.Hugo Herbelin
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch ||
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
Reviewed-by: gares
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
We will remove this modules and submit the overlays once the refactoring is done as to avoid churn.
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
This is needed to make this low-level entry structures privates; moreover, the code seems much clearer using the higher-level API. Some more cleanup needs to be done but this is clearly a step forward IMHO.
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
Porting them is still to be done, but at least we don't rely on the wrapper everywhere.
2020-05-03Wrap a monadic combinator in a try-with block to catch exceptions.Pierre-Marie Pédrot
Moving code around uncovered this bug.
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
This function was used almost everywhere with the wrapper around.
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the ↵Pierre Roux
same inductive) Numeral Notations now play better with multiple scopes for the same inductive. Previously, when multiple numeral notations where defined for the same inductive, only the last one was considered for printing. Now, we proceed as follows 1. keep only uninterpreters that produce an output (first List.map_filter) 2. keep only uninterpretation for scopes that either have a scope delimiter or are open (second List.map_filter) 3. the final selection is made according to the order of open scopes, (find_uninterpretation) or or according to the last defined notation if no appropriate scope is open (head of list at the end)
2020-05-02Move tclWRAPFINALLY to profile_ltacJason Gross
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef
2020-05-02Decrease LtacProf overhead when not profilingJason Gross
Note that this slightly changes the semantics of backtracking across `start ltac profiling`.
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
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
Reviewed-by: ppedrot
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
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 08:04:29 +0000