aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-27fix: Shorten ssrsetoid.vErik Martin-Dorel
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-12-11Remove the reliance of ring objects on the named part.Pierre-Marie Pédrot
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-06Make the string argument of `time` print correctlyJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:01:24 +0000