aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
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
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
2019-10-18factorize or_var_mapAlexandre Moine
2019-10-16Merge PR #10885: Remove [in_section] arguments to Safe_typing functionsPierre-Marie Pédrot
2019-10-14Fix coq#4741: Extract Constant/Inductive with JSONHelge Bahmann
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
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
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive projec...Frédéric Besson
2019-10-03Improved handling of micromega cachesFrédéric Besson
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
2019-09-25Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of introp...Pierre-Marie Pédrot
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
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-16Re-implementation of zifyFrédéric Besson
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-09-08more precise error messages for `Add Ring`Samuel Gruetter
2019-09-04Merge PR #10732: Make `Print Rings` and `Print Fields` more reliablethery
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-04Remove commented-out codeMaxime Dénès
2019-09-04Make `Print Rings` and `Print Fields` reliableMaxime Dénès
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
2019-09-02Merge PR #10716: [funind] Don't export duplicate save function.Pierre-Marie Pédrot
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
2019-08-29[funind] Don't export duplicate save function.Emilio Jesus Gallego Arias
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...Pierre-Marie Pédrot
2019-08-29Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exc...Pierre-Marie Pédrot
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10635: [funind] Port indfun to the new tactic engine.Pierre-Marie Pédrot
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-23[lemmas] Cleanup users of default proof information.Emilio Jesus Gallego Arias
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-22Merge PR #9062: Delay the computation of frozen evars in legacy unification.Matthieu Sozeau
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:55:54 +0000