aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-10Merge PR #11774: [exn] [nit] Remove not very useful re-raises.Pierre-Marie Pédrot
2020-03-09Merge PR #11787: Do not erase OCAMLPATH in CI targets with Dune-built CoqEmilio Jesus Gallego Arias
2020-03-09Merge PR #11720: Remove some productionlistsThéo Zimmermann
2020-03-09Remove some productionlistsJim Fehrle
2020-03-09Merge PR #11773: [doc] [dune] Update Dune build instructionsThéo Zimmermann
2020-03-09Do not erase OCAMLPATH in CI targets with Dune-built CoqMaxime Dénès
2020-03-08[doc] [dune] Update Dune build instructionsEmilio Jesus Gallego Arias
2020-03-08[exn] [nit] Remove not very useful re-raises.Emilio Jesus Gallego Arias
2020-03-08Merge PR #11578: [exn] Keep information from multiple extra exn handlersPierre-Marie Pédrot
2020-03-08Merge PR #11714: [gramlib] Refactor gramlib interface.Pierre-Marie Pédrot
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
2020-03-06Merge PR #11698: Fix #11592: Side effect safety may be broken by universe eff...Gaëtan Gilbert
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
2020-03-06Merge PR #11717: [dune] [ocamldebug] Improve ocamldebug rulesGaëtan Gilbert
2020-03-06Adding a test to the test-suite.Pierre-Marie Pédrot
2020-03-06Actually take advantage of the universes contained in side-effect certificates.Pierre-Marie Pédrot
2020-03-06Also check for monomorphic universes in side-effects certificates.Pierre-Marie Pédrot
2020-03-06Abstract away the API for side-effect certificates.Pierre-Marie Pédrot
2020-03-06Make explicit that the side-effect certificate trust is all-or-nothing.Pierre-Marie Pédrot
2020-03-05Merge PR #11744: [dune] Fix bug in auto-configure deps.Théo Zimmermann
2020-03-05Merge PR #11693: [boot] Don't initialize coqlib when `-boot` is passed.Enrico Tassi
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-05Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...Pierre-Marie Pédrot
2020-03-04Merge PR #11715: Be robust in calculating visible ids for non-registered cons...Hugo Herbelin
2020-03-04[boot] Don't initialize coqlib when `-boot` is passed.Emilio Jesus Gallego Arias
2020-03-04Merge PR #11429: [zify] several efficiency enhancementsVincent Laporte
2020-03-04Add overlay for equations.Hugo Herbelin
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
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[exn] Keep information from multiple extra exn handlersEmilio Jesus Gallego Arias
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-03[dune] Fix bug in auto-configure deps.Emilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-03-03[zify] efficiency improvementsFrédéric Besson
2020-03-03Ltac2: Add notation for enough and eenoughMichael Soegtrop
2020-03-03Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rstHugo Herbelin
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
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-02Refine patch for clearer scoping of evar_mapMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:52:11 +0000