aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-05-09Add a `with_strategy` tacticJason Gross
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
2020-05-09Merge PR #12204: Ltac helper functions APIHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with ↵Hugo Herbelin
multiple scopes for the same inductive)
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
Reviewed-by: maximedenes
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
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-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-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
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes #10951 for now and helps with #11492 .
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 05:36:00 +0000