aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-07-27Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distrHugo Herbelin
2019-07-26Merge PR #10563: changed name of cos3PI4 to cos_3PI4 for consistencyMichael Soegtrop
2019-07-26Merge PR #10568: Mark primitive integers as able to participate in reductions...Maxime Dénès
2019-07-25[Int63] Remove redundant misnamed lemma lsr_add_distrVincent Laporte
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
2019-07-24changed name of cos3PI4 to cos_3PI4 for consistencyRobert Rand
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in re...Enrico Tassi
2019-07-24Merge PR #10549: [lemmas] Small cleanupsGaëtan Gilbert
2019-07-24Merge PR #10537: [vernacexpr] Refactor fixpoint AST.Gaëtan Gilbert
2019-07-23Merge PR #10552: Fix a detail in 2 doc files for the under tacticThéo Zimmermann
2019-07-23[obligations] Use already existing type alias.Emilio Jesus Gallego Arias
2019-07-23[lemmas] save_remaining_recthms doesn't need a norm parameter.Emilio Jesus Gallego Arias
2019-07-23[lemmas] Refactor code a bit, saving functions now to in the saving part.Emilio Jesus Gallego Arias
2019-07-23Merge PR #10554: Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Enrico Tassi
2019-07-23[funind] Remove single-shot type alias.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-07-23Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Pierre-Marie Pédrot
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
2019-07-23Merge PR #10541: Dune: fix build_all_stdlib ruleEmilio Jesus Gallego Arias
2019-07-22Merge PR #10447: Refactor and expand contributing guide.Maxime Dénès
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
2019-07-22Merge PR #10462: [Pretyping] Do not restrict a solved evarEnrico Tassi
2019-07-22Merge PR #10522: Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and ...Maxime Dénès
2019-07-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
2019-07-21Dune: do not use with-outputs-to for shimsGaëtan Gilbert
2019-07-21Dune: fix build_all_stdlib ruleGaëtan Gilbert
2019-07-20Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg fil...Théo Zimmermann
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
2019-07-19Merge PR #10521: Move unfold_side_flags CClosure -> Tacred internalsPierre-Marie Pédrot
2019-07-19Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewriteGaëtan Gilbert
2019-07-19Removed patches for Flocq, Interval and Gappa (merged upstream)Michael Soegtrop
2019-07-19Merge PR #10532: [doc] Fix typo in doc/sphinx/addendum/ring.rstthery
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-18Adding overlays.Pierre-Marie Pédrot
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-18Polymorphism attribute on section sets the option locally.Pierre-Marie Pédrot
2019-07-18Remove dead code in Lib.Pierre-Marie Pédrot
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2019-07-18Use a dedicated data structure for section representation in Lib.Pierre-Marie Pédrot
2019-07-17Merge PR #10518: [funind] Remove unneeded callback.Pierre-Marie Pédrot
2019-07-17Fixed Windows patch for QuickchickMichael Soegtrop
2019-07-17Adjust VST patch to latest changes in VSTMichael Soegtrop
2019-07-17Make windows build fail immediately if plugin patches failMichael Soegtrop
2019-07-16Removed patch for Gappa tool (verified that changes in gappa master fixed the...Michael Soegtrop
2019-07-16Enable Coquelicot, Flocq, Interval and Gappa in extended/release Windows buildsMichael Soegtrop
2019-07-16Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)Michael Soegtrop
2019-07-16Move unfold_side_flags CClosure -> Tacred internalsGaëtan Gilbert
2019-07-16Merge PR #10520: Fix typosThéo Zimmermann
2019-07-15TyposJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:04:28 +0000