aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-04Fix #11749: don't warn for hidden files.Théo Zimmermann
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-04Add file to register names of reals library used by gappaMichael Soegtrop
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-03Remove invisible U+FE00 variation selector from CoqIDE bindingsNickolai Zeldovich
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-03When parsing negative integer, ensure minus sign is contiguous to the number.Hugo Herbelin
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-03Update the OCaml version in `default.nix` to 4.09.0Maxime Dénès
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
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-03-01test-suite file for spurious universe generationMatthieu Sozeau
2020-03-01Fix mishandling of sigma in guess_elim (regression from 8.11)Matthieu Sozeau
2020-02-29[dune] [ocamldebug] Improve ocamldebug rulesEmilio Jesus Gallego Arias
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
2020-02-29Be robust in calculating visible ids for non-registered constants.Pierre-Marie Pédrot
2020-02-28Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compilingHugo Herbelin
2020-02-28[gramlib] Refactor gramlib interface.Emilio Jesus Gallego Arias
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-28Deprecate the OCaml API to declare term Hints.Pierre-Marie Pédrot