aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-10-22FSetEqProperties: do not use “omega”Vincent Laporte
2019-10-22OrderedTypeEx: do not use “omega”Vincent Laporte
2019-10-22Zpower: do not use “omega”Vincent Laporte
2019-10-22Lia: make explicit which “zify” is usedVincent Laporte
2019-10-22ZMicromega: do not use “omega”Vincent Laporte
2019-10-22Qround: do not use “omega”Vincent Laporte
2019-10-22Qreduction: do not use “omega”Vincent Laporte
2019-10-22QArith_base: do not use “omega”Vincent Laporte
2019-10-22FSets: do not use “omega”Vincent Laporte
2019-10-22Znumtheory: do not use “omega”Vincent Laporte
2019-10-22Zdiv: do not use “omega”Vincent Laporte
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-10-22Merge PR #10787: Fix #10779 (hnf normalisation of instance + reification of o...Vincent Laporte
2019-10-21Improvements of zifyFrédéric Besson
2019-10-21Merge PR #10857: Fix votour after the change of representation of opaques.Maxime Dénès
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-18Merge PR #10914: Fix Locate printing regressionHugo Herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ...Gaëtan Gilbert
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-18Merge PR #10919: factorize or_var_mapPierre-Marie Pédrot
2019-10-18Merge PR #10913: re-expose UState.demote_seff_univsPierre-Marie Pédrot
2019-10-18Merge PR #8228: (Partially) Revert "Make Environ.globals abstract."Pierre-Marie Pédrot
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and clas...Pierre-Marie Pédrot
2019-10-18factorize or_var_mapAlexandre Moine
2019-10-18Merge PR #10915: Fix link to `xml-protocol.md` in `dev/README.md`Théo Zimmermann
2019-10-18Fix votour after the change of representation of opaques.Pierre-Marie Pédrot
2019-10-17Fix link to `xml-protocol.md` in `dev/README.md`Michael D. Adams
2019-10-17Fix Locate printing regressionGuillaume Melquiond
2019-10-16re-expose UState.demote_seff_univsGaëtan Gilbert
2019-10-16Merge PR #10885: Remove [in_section] arguments to Safe_typing functionsPierre-Marie Pédrot
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-16Define sphinx replacements for \SProp \Type etcGaëtan Gilbert
2019-10-16Merge PR #10896: Assign ownership of the test-suite compat filesThéo Zimmermann
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
2019-10-14Assign ownership of the test-suite compat filesJason Gross
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
2019-10-14Merge PR #10852: Fix #10842: incorrect handling of unicode input before spacePierre-Marie Pédrot
2019-10-14Updating changelogHugo Herbelin
2019-10-14ClassicalFacts.v: Unifying format for bibliographical references.Hugo Herbelin
2019-10-14Weak excluded-middle: adding a reference.Hugo Herbelin
2019-10-14Logic: Add equivalence between weak excluded-middle and classical Morgan's lawHugo Herbelin
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
2019-10-14Remove obj_sec field of Nametab.obj_prefix record.Gaëtan Gilbert
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
2019-10-14Merge PR #10887: fix rev_right_loop docEnrico Tassi