aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-24fix «W -- weakening» docAntonio Nikishaev
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-18Adding `inj_compr` lemma in ssrfun.Cyril Cohen
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-16Merge PR #10998: Add missing zify class instancesFrédéric Besson
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-11-01[ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded)Erik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
2019-10-31lra: use “lia” rather than “omega”Vincent Laporte
2019-10-31[ssr] Refactor/Simplify the implementation of underErik Martin-Dorel
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-26Merge PR #10516: [funind] Remove duplicate save function.Gaëtan Gilbert
2019-10-25Add 2 missing instances in ZifyBool.vKazuhiko Sakaguchi
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-23Merge PR #10932: Add a notation for the empty type.Théo Zimmermann
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
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-21chore: Enclose the […get_reflexive_proof_ssr…] call in a try/with->assert...Erik Martin-Dorel
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:35:29 +0000