aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-29Merge PR #11184: Undeprecate Add Setoid / Add Morphism.Pierre-Marie Pédrot
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-29Merge PR #11186: Remove undocumented and deprecated `Congruence Depth` optionPierre-Marie Pédrot
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
2019-11-26Remove undocumented and deprecated `Congruence Depth` optionMaxime Dénès
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-26Undeprecate Add Setoid / Add Morphism.Théo Zimmermann
2019-11-25Nsatz: use “lia” rather than “omega”Vincent Laporte
2019-11-25setoid_ring: do not use “omega”Vincent Laporte
2019-11-25zify: explicitly use “lia”Vincent Laporte
2019-11-25btauto: use “lia” rather than “omega”Vincent Laporte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:56:45 +0000