aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
2019-07-22Merge PR #10447: Refactor and expand contributing guide.Maxime Dénès
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
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-19[vernac] [inductive] Remove unused functions/exports.Emilio Jesus Gallego Arias
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-18Shorten changelogVincent Semeria
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-17Rename ConstructiveRIneq and ConstructiveRcompleteVincent Semeria
2019-07-16Removed patch for Gappa tool (verified that changes in gappa master fixed the...Michael Soegtrop
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
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
2019-07-15[funind] Remove unneeded callback.Emilio Jesus Gallego Arias
2019-07-15Merge PR #10517: Azure CI MacOS: build byte target firstEmilio Jesus Gallego Arias
2019-07-15Azure CI MacOS: build byte target firstGaëtan Gilbert
2019-07-15Merge PR #10512: Remove Stm.call_process_error_oncePierre-Marie Pédrot
2019-07-14Merge PR #10496: [proof] Minor cleanup in proof.mlPierre-Marie Pédrot
2019-07-11Merge PR #10424: Update doc for % escapes in Sphinx, improve error messagesClément Pit-Claudel
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-07-11Merge PR #10510: Fixed a few wrong reference and typosThéo Zimmermann
2019-07-11Remove Stm.call_process_error_onceGaëtan Gilbert
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-11Refactor the part about contributing to the stdlib.Théo Zimmermann
2019-07-11More positive wording of the foreword to the contributing guide.Théo Zimmermann
2019-07-11Improve contributing guide further following reviewers' comments.Théo Zimmermann
2019-07-11Refactor and expand contributing guide.Théo Zimmermann