aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-17[ci] Add travis setup, docker-based.Emilio Jesus Gallego Arias
Pretty straightforward; need to be enabled in the Travis console tho.
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
Fix for coq/coq#8515 (command driven attributes)
2018-11-03Merge pull request coq/ltac2#82 from SkySkimmer/split-tacticsPierre-Marie Pédrot
Adapt to coq/coq#8844 (move abstract out of tactics.ml)
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
This allows to drop the ltac2 folder inside the Coq dir and have it compose with the Coq build. I've fixed build warnings by the way.
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
Fix for compilation with the camlp5-parser branch.
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
Adapt to coq/coq#7558.
2018-05-28Fix w.r.t. coq/coq#7521.Pierre-Marie Pédrot
2018-05-27Adapt to coq/coq#7558.Emilio Jesus Gallego Arias
Trivial renaming of the vernacular parsing entry point.
2018-05-25Renaming global_reference according to Coq PR #6156.Hugo Herbelin
2018-05-25Renaming smartmap and fold_map according to Coq PR #7177.Hugo Herbelin
2018-05-25Merge pull request coq/ltac2#58 from ejgallego/tactics+push_fix_naming_outPierre-Marie Pédrot
Adapt to fix/cofix changes in Coq (coq/coq#7196)
2018-05-24Adapt to fix/cofix changes in Coq (coq/coq#7196)Emilio Jesus Gallego Arias
c.f. https://github.com/coq/coq/pull/7196
2018-05-15Merge branch 'fast-constr-match-no-context'Pierre-Marie Pédrot
2018-04-24Merge pull request coq/ltac2#50 from Armael/fix-typoPierre-Marie Pédrot
Fix another typo in the documentation's grammar for open variants
2018-04-19Allowing formatting break around a printed type.Hugo Herbelin
2018-04-19Fixing printing level for subtypes of a type constructor.Hugo Herbelin
2018-04-11Fix compilation w.r.t. coq/coq#7213.Pierre-Marie Pédrot
2018-04-06Merge pull request coq/ltac2#52 from ejgallego/ltac+tacdeprPierre-Marie Pédrot
[coq] Adapt to coq/coq#6960.
2018-04-02[coq] Adapt to coq/coq#6960.Emilio Jesus Gallego Arias
Minor, a couple of tactic-related types moved.
2018-03-27Fix printing of toplevel record values.Pierre-Marie Pédrot
2018-03-27Fixup strict mode for patternsPierre-Marie Pédrot
2018-03-13Fix another typo in the documentation's grammar for open variantsArmael
2018-03-13Merge pull request coq/ltac2#49 from Armael/fix-typoPierre-Marie Pédrot
Fix a typo
2018-03-13Fix a typoArmael
2018-03-10Merge pull request coq/ltac2#46 from ejgallego/located+libnamesPierre-Marie Pédrot
[coq] Adapt to coq/coq#6837.
2018-03-10Merge pull request coq/ltac2#47 from ejgallego/ssr+correct_packingPierre-Marie Pédrot
[coq] Adapt to correct LTAC module packing coq/coq#6869
2018-03-10[coq] Adapt to coq/coq#6837.Emilio Jesus Gallego Arias
Minor.
2018-03-10[coq] Adapt to coq/coq#6831.Emilio Jesus Gallego Arias
This removes uses of `Loc.t` in favor of `CAst.t`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-16 15:52:27 +0000