aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
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 .
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
This moves the vernacular part of hints to `vernac`; in particular, it helps removing the declaration of constants as parts of the `tactic` folder.
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables ↵Lysxia
(incidentally fixes #7697) Reviewed-by: Lysxia
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
This provides linking, appropriate coloring and appropriate hovering in coqdoc documents. In particular, this fixes #7697.
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
This still needs API cleanup but we defer it to the moment we are ready to make the internals private.
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
If we remove all the legacy proof engine stuff, that would remove the need for the view on proof almost entirely.
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
We place creation and saving of interactive proofs in the same module; this will allow to make `proof_entry` private, improving invariants and control over clients, and to reduce the API [for example next commit will move abstract declaration into this module, removing the exported ad-hoc `build_constant_by_tactic`] Next step will be to unify all the common code in the interactive / non-interactive case; but we need to tweak the handling of obligations first.
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
This actually gets `Pfedit` out of the dependency picture [can be almost merged with `Proof` now, as it is what it manipulates] and would allow to reduce the exported low-level API from `Proof_global`, as `map_fold_proof` is not used anymore.
2020-04-15Merge PR #11776: [ocamlformat] Enable for funind.Pierre Courtieu
Reviewed-by: Matafou Ack-by: Zimmi48 Ack-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 18:45:30 +0000