aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-01Merge PR #12217: Fix #12215: ci scripts naming inconsistenciesEmilio Jesus Gallego Arias
2020-05-01Merge PR #12222: Less confusing configure message when lablgtk exists but not...Emilio Jesus Gallego Arias
2020-05-01do not re-export ListNotations from Program: vst overlayAntonio Nikishaev
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
2020-04-30Less confusing configure message when lablgtk exists but not lablgtksourceview.Hugo Herbelin
2020-04-30Merge PR #12213: [zify] add support for Nat.le, Nat.lt and Nat.eqVincent Laporte
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-30Merge PR #12216: Remove outdated code and comments in Declare.Emilio Jesus Gallego Arias
2020-04-30Move availability_of_prim_tokenPierre Roux
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-30Remove outdated code and comments in Declare.Pierre-Marie Pédrot
2020-04-30Symmetry in conclusions of List.map_eq_*Olivier Laurent
2020-04-30Merge PR #12208: Reduce rational numbers in Cauchy real addition, to accelera...Michael Soegtrop
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2020-04-30do not re-export ListNotations from Program: changelogAntonio Nikishaev
2020-04-30do not re-export ListNotations from Program: overlaysAntonio Nikishaev
2020-04-30do not re-export ListNotations from ProgramAntonio Nikishaev
2020-04-29When TIMED=1, emit timing info for OCaml filesJason Gross
2020-04-29Merge PR #12209: Merge duplicates in .mailmapThéo Zimmermann
2020-04-29Merge duplicates in .mailmapJason Gross
2020-04-29Reduce rational numbers in Cauchy real addition, to accelerate itVincent Semeria
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ...Emilio Jesus Gallego Arias
2020-04-29Merge PR #12198: CI: change ext-lib url, it is at coq-community nowEmilio Jesus Gallego Arias
2020-04-29Merge PR #12202: Centralize the call to `tclEFFECTS` in scheme declarationEmilio Jesus Gallego Arias
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ...Clément Pit-Claudel
2020-04-29Merge PR #12158: [univ] API to demote global universesMatthieu Sozeau
2020-04-29Merge PR #12195: [doc] [sphinx] Run in silent mode by defaultThéo Zimmermann
2020-04-29Merge PR #12174: [ci] Add coq-tools to the CIThéo Zimmermann
2020-04-29Support in-line glossary entries and referencesJim Fehrle
2020-04-29Merge PR #12203: [ci] [doc] misspelled script name create_overlays.shThéo Zimmermann
2020-04-29[univ] API to demote global universesEnrico Tassi
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
2020-04-29Remove dead user-facing code in scheme generation.Pierre-Marie Pédrot
2020-04-29CI: ext-lib is at coq-community nowAntonio Nikishaev
2020-04-28Merge PR #12193: Close files in fetch_delayedEmilio Jesus Gallego Arias
2020-04-28[doc] [sphinx] Be silent when running latexmkEmilio Jesus Gallego Arias
2020-04-28[doc] [sphinx] Run in silent mode by defaultEmilio Jesus Gallego Arias
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
2020-04-28Merge PR #12164: Stop relying on side-effects for recursive scheme declarationEmilio Jesus Gallego Arias
2020-04-28Add comment about decide equality dependence computation.Pierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-28Merge PR #12188: Do not delay the loading of the library_disk field when requ...Emilio Jesus Gallego Arias
2020-04-28Merge PR #12189: Fix an ordering bug in the CODEOWNERS file following #11529.Emilio Jesus Gallego Arias
2020-04-28Close files in fetch_delayedGaëtan Gilbert
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann