aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-04Merge PR #11618: [loadpath] Rework and simplify ML loadpath handlingThéo Zimmermann
2020-03-04Merge PR #11709: Deprecate the "prolog" tactic.Théo Zimmermann
2020-03-03[vernac] Use a record for VernacAddLoadPathEmilio Jesus Gallego Arias
2020-03-03[stm] Port documentation of init options to ocamldocEmilio Jesus Gallego Arias
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-03Merge PR #11695: Refactor lookaheadsPierre-Marie Pédrot
2020-03-02Merge PR #11634: Remove the dependency in float.cmo and uint63.cmo for buildi...Pierre-Marie Pédrot
2020-03-02Merge PR #11681: Fix backtraces in conversion anomalies caught by Reductionops.Maxime Dénès
2020-03-02Merge PR #11728: [dune] [doc] Be more explicit about coqtop dependenciesThéo Zimmermann
2020-03-01Merge PR #11708: [ci] elpi 1.10.2Emilio Jesus Gallego Arias
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-03-01Move lookahead combinators to PcoqMaxime Dénès
2020-03-01[ci] [docker] overlay for elpi 1.10Enrico Tassi
2020-03-01[ci] [docker] bump elpi to 1.10.2Enrico Tassi
2020-03-01[ci] bump dune to 2.0.1 due to upstream problemsEnrico Tassi
2020-03-01[dune] [doc] Be more explicit coqtop dependenciesEmilio Jesus Gallego Arias
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
2020-02-28Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compilingHugo Herbelin
2020-02-28Merge PR #11423: Convert Vernacular section of gallina chapter to use prodnThéo Zimmermann
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-28Deprecate the "prolog" tactic.Pierre-Marie Pédrot
2020-02-28Merge PR #11609: [stm] Use Default Proof Using only with ProofEnrico Tassi
2020-02-28[stm] Use Default Proof Using only with ProofTej Chajed
2020-02-28Adding change logHugo Herbelin
2020-02-28Makefile in test-suite: More separation of concerns as suggested by Enrico.Hugo Herbelin
2020-02-28Fixed some escaping problems with arguments containing spaces in IDE's Compil...Ike Mulder
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-27Fix #11696: link from refman to stdlib doc is dead.Théo Zimmermann
2020-02-27Merge PR #11581: [native compiler] Add options to set object directories.Maxime Dénès
2020-02-26[native compiler] Allow to set OCaml include dirs for compilationEmilio Jesus Gallego Arias
2020-02-26[native compiler] Allow to set the output directory for cmx objectsEmilio Jesus Gallego Arias
2020-02-26Merge PR #11644: Use implicit arguments in notations for eq.Hugo Herbelin
2020-02-26Merge PR #11687: Fix changelog for https://github.com/coq/coq/pull/11686Théo Zimmermann
2020-02-26Addr 'attr' directive for attributesJim Fehrle
2020-02-26Fix changelog for https://github.com/coq/coq/pull/11686Maxime Dénès
2020-02-26Merge PR #11686: Consolidate int63-related notationsthery
2020-02-26Consolidate int63-related notationsMaxime Dénès
2020-02-25Merge PR #11680: Fixing residual bug of #11120: inheritance of maximal implic...Emilio Jesus Gallego Arias
2020-02-25Merge PR #11663: Remove unqualified universe attributes.Emilio Jesus Gallego Arias
2020-02-25Merge PR #11669: Remove hard to read blue color in merge-prEmilio Jesus Gallego Arias
2020-02-25Fix backtraces in conversion anomalies caught by Reductionops.Pierre-Marie Pédrot
2020-02-25Merge PR #11674: [ci] Fix Coquelicot buildGaëtan Gilbert
2020-02-25Merge PR #11666: Do not perform a universe diff when typing opaque constants.Gaëtan Gilbert
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
2020-02-25Merge PR #11432: More portable C flagsMaxime Dénès
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...Pierre-Marie Pédrot
2020-02-25Merge PR #11489: [exn] remove `raise` taking optional exception information a...Pierre-Marie Pédrot
2020-02-25Merge PR #11675: Make it clear how to import Ltac2Théo Zimmermann
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot