aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
2020-02-08Merge PR #10343: Resolve 10342 : [Ltac2] Add array libraryPierre-Marie Pédrot
2020-02-08Merge PR #11404: replace RList by list R in all files where it is used in thi...Pierre-Marie Pédrot
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-07Merge PR #11523: [coqdep] Several refactoring and consolidationsGaëtan Gilbert
2020-02-07Merge PR #11528: Checker does not rely on Monomorphic fieldsGaëtan Gilbert
2020-02-07[coqdep] Add changelog for recent modifications.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Don't treat stdlib specially in boot mode.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Remove deprecated -slash , unused, undocumented -mldep option.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Remove dumpgraph and broken optionsEmilio Jesus Gallego Arias
2020-02-07Merge PR #11543: restore the default URL for coquelicotThéo Zimmermann
2020-02-07restore the default URL for coquelicotYves Bertot
2020-02-06replace RList by list RYves Bertot
2020-02-06Merge PR #11458: Don't install doc_grammarEnrico Tassi
2020-02-06Merge PR #11478: Nicer kernel universe error for inductivesPierre-Marie Pédrot
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive notati...Pierre-Marie Pédrot
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
2020-02-05Remove a dubious part of the checker code relying on a universe contextPierre-Marie Pédrot
2020-02-05Store the template polymorphic context inside the TemplateArity node.Pierre-Marie Pédrot
2020-02-05Merge PR #11511: Delay lifting in Evarsolve aliasing.Enrico Tassi
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
2020-02-04Merge PR #11513: Test for #5617: Primitive projections confuse the terminatio...Gaëtan Gilbert
2020-02-04Merge PR #11514: add regression test for liaPierre-Marie Pédrot
2020-02-04Merge PR #11474: Fix efficiency regression #11436Vincent Laporte
2020-02-03add regression test for liaAndres Erbsen
2020-02-03Merge PR #11508: [ci] [fiat-crypto] Use the pinned bedrock2Emilio Jesus Gallego Arias
2020-02-03Test for #5617: Primitive projections confuse the termination checker.Pierre-Marie Pédrot
2020-02-03Do not return a full term in Evarsolve alias expansion.Pierre-Marie Pédrot
2020-02-03Delay lifting in Evarsolve aliasing.Pierre-Marie Pédrot
2020-02-03Merge PR #11497: [opam] Don't disable native compute in opam.dev fileGaëtan Gilbert
2020-02-03Merge PR #11493: [makefile] Ignore _build_boot directoryGaëtan Gilbert
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-02-03Merge PR #11481: Do not rely on Libobject for the current environment in extr...Maxime Dénès
2020-02-03Merge PR #11490: [exn] Don't reraise in exception printersPierre-Marie Pédrot
2020-02-02[ci] [fiat-crypto] Use the pinned bedrock2Jason Gross
2020-02-02Merge PR #11500: [ci] [fiat-crypto-legacy] Use new, faster targetsEmilio Jesus Gallego Arias
2020-02-02Merge PR #11484: Fix 11483 (Performance bug of PrimFLoat.compare with native_...Pierre-Marie Pédrot
2020-02-02Merge PR #11326: Refactoring part of #11120 about printing applied global ref...Emilio Jesus Gallego Arias
2020-02-02Merge PR #11466: checkdeps.py: add missing dep & report deps all at onceThéo Zimmermann
2020-01-31[ci] [fiat-crypto-legacy] Use new, faster targetsJason Gross
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
2020-01-31[opam] Don't disable native compute in opam.dev fileEmilio Jesus Gallego Arias
2020-01-31[makefile] Ignore _build_boot directoryEmilio Jesus Gallego Arias
2020-01-30Factorize export_private_constants + register_side_effectGaëtan Gilbert
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Notations: Fixing a wrong location in format.Hugo Herbelin
2020-01-30Constrextern.ml: Move a function earlier to be usable for pattern printing.Hugo Herbelin
2020-01-30Minor indentation change.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-20 20:18:02 +0000