aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional ↵Hugo Herbelin
extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes
2019-10-26Merge PR #10516: [funind] Remove duplicate save function.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2019-10-25Add 2 missing instances in ZifyBool.vKazuhiko Sakaguchi
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
AFAICT the reasoning for introducing this function doesn't hold anymore. This is needed for future refactorings that should make some types private.
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ↵Vincent Semeria
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
2019-10-23Merge PR #10932: Add a notation for the empty type.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: amahboubi
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
Reviewed-by: vbgl
2019-10-22Add a notation for the empty type.Arthur Azevedo de Amorim
2019-10-22Lia: make explicit which “zify” is usedVincent Laporte
2019-10-22ZMicromega: do not use “omega”Vincent Laporte
2019-10-21Improvements of zifyFrédéric Besson
- Fix reification of overloaded operators (triggers convertibility checks with existing terms) - Zify instances need not be in hnf - Fix specification of bool operators - Add (limited) support for comparison fixes #10779
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-18factorize or_var_mapAlexandre Moine
2019-10-16Merge PR #10885: Remove [in_section] arguments to Safe_typing functionsPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-14Fix coq#4741: Extract Constant/Inductive with JSONHelge Bahmann
Resolve by consulting is_custom/find_custom.
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
AFAICT there is no reason to use interp_open_constr I used Evd.from_ctx to keep passing evar maps around but maybe we should be passing ustates instead?
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-13fix rev_right_loop docAntonio Nikishaev
2019-10-11Merge PR #10740: More precise error messages for `Add Ring`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive ↵Frédéric Besson
projections Reviewed-by: fajb
2019-10-03Improved handling of micromega cachesFrédéric Besson
- Specialised hash and equality functions. Avoid collisions in extreme scenarios. - Flags to disable the use of the caches. fixes #10772
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-29Merge PR #10673: [lemmas] Cleanup users of default proof information.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-09-25Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of ↵Pierre-Marie Pédrot
intropattern entry in #10239) Reviewed-by: ppedrot
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-23Fixes #10778 (fresh was not updated after renaming of intropattern entry in ↵Hugo Herbelin
#10239). The bug was introduced in #10239 which seems to have actually remained half-done: "wit_intropattern" and "wit_simple_intropattern" did not share the same representation of values (val_tag) but the code was assuming (especially the code for "fresh") that this was shared. We fix it by sharing the internal representation (`dyn` field in Tacarg.make0) as suggested by @ppedrot in the discussion of #10239 (this allows also to simplify Taccoerce.is_intro_pattern).
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot Ack-by: vbgl
2019-09-16Re-implementation of zifyFrédéric Besson
The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
Libraries are now handled like other modules.
2019-09-08more precise error messages for `Add Ring`Samuel Gruetter
2019-09-04Merge PR #10732: Make `Print Rings` and `Print Fields` more reliablethery
Reviewed-by: thery
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
2019-09-04Remove commented-out codeMaxime Dénès
2019-09-04Make `Print Rings` and `Print Fields` reliableMaxime Dénès
Previously, they were using a map that was different from the one used by the real lookup, leading to confusing information (number of instances could be wrong, etc).
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
Reviewed-by: gares
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
Reviewed-by: maximedenes
2019-09-02Merge PR #10716: [funind] Don't export duplicate save function.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: herbelin Ack-by: mattam82 Reviewed-by: ppedrot
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
Matthieu Sozeau explained how to fix this.
2019-08-29[funind] Don't export duplicate save function.Emilio Jesus Gallego Arias
It will take a bit more to clean up the mess with entries in the `indfun` plugin [quite a few PRs in the queue], but thanks to recent refactoring the tricky parts are self-contained now in `gen_principle` so we can remove the duplicated `save` function from the public API.
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ↵Pierre-Marie Pédrot
proof data on top of declare. Reviewed-by: ppedrot
2019-08-29Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify ↵Pierre-Marie Pédrot
exception names Reviewed-by: ppedrot
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
As documented in the feedback API.
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
Non-delayed entries can be done with the current constructor, delayed ones will require more work.
2019-08-27Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on ↵Emilio Jesus Gallego Arias
top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 01:44:41 +0000