aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2019-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
(as suggested by @silene)
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
Beware of 0. = -0. issue for primitive floats The IEEE 754 declares that 0. and -0. are treated equal but we cannot say that this is true with Leibniz equality. Therefore we must patch the equality and the total comparison inside the kernel to prevent inconsistency.
2019-10-31lra: use “lia” rather than “omega”Vincent Laporte
2019-10-31lia: depend only on ZArith_baseVincent Laporte
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 15:37:28 +0000