aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-04-04Adapt to coq/coq#8764Pierre Roux
2019-04-02Merge pull request coq/ltac2#118 from vbgl/rm-hardwired-hint-dbPierre-Marie Pédrot
2019-04-02Merge pull request coq/ltac2#117 from ejgallego/opam_updatePierre-Marie Pédrot
2019-04-02[opam] Update file to newer format and build system.Emilio Jesus Gallego Arias
2019-04-01Merge pull request coq/ltac2#114 from proux01/token-typePierre-Marie Pédrot
2019-03-31Merge pull request coq/ltac2#112 from gares/quotationsPierre-Marie Pédrot
2019-03-31[coq] Adapt to coq/coq#9815Pierre Roux
2019-03-31overlay for PR 9733Enrico Tassi
2019-03-30Merge pull request coq/ltac2#86 from ejgallego/more-dunePierre-Marie Pédrot
2019-03-29[dune] Full Dune support.Emilio Jesus Gallego Arias
2019-03-28Merge pull request coq/ltac2#109 from ejgallego/proof+no_global_partialPierre-Marie Pédrot
2019-03-26Fix for https://github.com/coq/coq/pull/8984Vincent Laporte
2019-03-20[coq] Adapt to coq/coq#9129 "removal of imperative proof state"Emilio Jesus Gallego Arias
2019-03-20Merge pull request coq/ltac2#113 from maximedenes/printed-by-envPierre-Marie Pédrot
2019-03-19Adapt to changes in Coq's printers APIMaxime Dénès
2019-03-15Merge pull request coq/ltac2#93 from SkySkimmer/spropPierre-Marie Pédrot
2019-02-20Merge pull request coq/ltac2#108 from ejgallego/fix_warnPierre-Marie Pédrot
2019-02-20[coq] Fix OCaml warnings.Emilio Jesus Gallego Arias
2019-02-14Adapt to coq/coq#8817 (SProp)Gaëtan Gilbert
2019-02-13Merge pull request coq/ltac2#92 from ejgallego/proofview+proof_infoPierre-Marie Pédrot
2019-02-09[coq] Adapt to coq/coq#9137Emilio Jesus Gallego Arias
2019-02-09Merge pull request coq/ltac2#102 from maximedenes/rm-unknownPierre-Marie Pédrot
2019-02-08Remove VtUnknown classificationMaxime Dénès
2019-02-08Merge pull request coq/ltac2#101 from maximedenes/program-mode-flagPierre-Marie Pédrot
2019-02-01Adapt to https://github.com/coq/coq/pull/9410Maxime Dénès
2019-01-30Merge pull request coq/ltac2#100 from JasonGross/fix-lazy-match-goalPierre-Marie Pédrot
2019-01-28Make lazy_match! goal actually lazyJason Gross
2019-01-28Merge pull request coq/ltac2#94 from maximedenes/proof-modePierre-Marie Pédrot
2019-01-17Adapt to Coq's new proof mode APIMaxime Dénès
2018-12-16Merge pull request coq/ltac2#91 from ejgallego/proof_reworkPierre-Marie Pédrot
2018-12-10[coq] Adapt to coq/coq#9172Emilio Jesus Gallego Arias
2018-12-06Merge pull request coq/ltac2#90 from ejgallego/testsPierre-Marie Pédrot
2018-11-28[build] Test tests in Travis, use coqc for tests.Emilio Jesus Gallego Arias
2018-11-25Merge pull request coq/ltac2#88 from wilcoxjay/tests-detect-coqbinPierre-Marie Pédrot
2018-11-24tests/Makefile: support unset COQBIN, like top-level Makefile doesJames R. Wilcox
2018-11-24Merge pull request coq/ltac2#87 from ppedrot/camlp5-safe-api-strikes-backPierre-Marie Pédrot
2018-11-23Fix w.r.t. coq/coq#9051.Pierre-Marie Pédrot
2018-11-19Merge remote-tracking branch 'origin/pr/84'Pierre-Marie Pédrot
2018-11-19Adding a module to manipulate Ltac1 values.Pierre-Marie Pédrot
2018-11-19Add a function to generate fresh reference instances.Pierre-Marie Pédrot
2018-11-19Add a Char module.Pierre-Marie Pédrot
2018-11-17Add an image status for the CI.Pierre-Marie Pédrot
2018-11-17Merge pull request coq/ltac2#85 from ejgallego/travisPierre-Marie Pédrot
2018-11-17[ci] Add travis setup, docker-based.Emilio Jesus Gallego Arias
2018-11-17[coq] Overlay to adapt to coq/coq#9003Emilio Jesus Gallego Arias
2018-11-15Fix compilation w.r.t. coq/coq#8779.Pierre-Marie Pédrot
2018-11-13Port to coqpp.Pierre-Marie Pédrot
2018-11-05Merge pull request coq/ltac2#75 from SkySkimmer/command-attsPierre-Marie Pédrot
2018-11-03Merge pull request coq/ltac2#82 from SkySkimmer/split-tacticsPierre-Marie Pédrot
2018-10-30Adapt to coq/coq#8844 (move abstract out of tactics.ml)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 01:20:03 +0000