aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-10-23Merge remote-tracking branch 'origin/pr/70'Pierre-Marie Pédrot
2018-10-23Merge remote-tracking branch 'origin/pr/71'Pierre-Marie Pédrot
2018-10-17[build] Add dune file + fix warnings.Emilio Jesus Gallego Arias
2018-10-11Fix for coq/coq#8515 (command driven attributes)Gaëtan Gilbert
2018-10-08Merge remote-tracking branch 'remotes/origin/pr/74'Pierre-Marie Pédrot
2018-10-06Merge remote-tracking branch 'maximedenes/rm-section-path'Pierre-Marie Pédrot
2018-10-02Fix deprecation warnings.Pierre-Marie Pédrot
2018-09-26Adapt to removal of section paths from kernel namesMaxime Dénès
2018-09-26Fix for Coq PR#8554 (term builder for tactic "change" takes an environment).Hugo Herbelin
2018-09-11Merge remote-tracking branch 'herbelin/master+globenv-coq-pr7288'Pierre-Marie Pédrot
2018-08-07fix three small typosLangston Barrett
2018-08-07doc/ltac2.md: add table of contentsLangston Barrett
2018-07-23Adding environment-manipulating functions.Pierre-Marie Pédrot
2018-07-23Fix deprecated warnings from Pcoq.Pierre-Marie Pédrot
2018-07-23Merge remote-tracking branch 'origin/pr/54'Pierre-Marie Pédrot
2018-07-04Adapting to move of register_constr_interp0 from Pretyping to GlobEnv.Hugo Herbelin
2018-07-02Merge pull request coq/ltac2#65 from ppedrot/camlp5-parserPierre-Marie Pédrot
2018-06-23Fix for compilation with the camlp5-parser branch.Pierre-Marie Pédrot
2018-06-18Adapt to Coq's PR #7797 (removal of reference).Maxime Dénès
2018-06-18Do not rely on the Ident vs. Qualid artificial separation.Pierre-Marie Pédrot
2018-06-18Fixing a batch of deprecation warnings.Pierre-Marie Pédrot
2018-05-30Merge pull request coq/ltac2#60 from ejgallego/vernac+move_parserPierre-Marie Pédrot
2018-05-28Fix w.r.t. coq/coq#7521.Pierre-Marie Pédrot
2018-05-27Adapt to coq/coq#7558.Emilio Jesus Gallego Arias
2018-05-25Renaming global_reference according to Coq PR #6156.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 23:54:09 +0000