aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-10-30Adapt to coq/coq#8844 (move abstract out of tactics.ml)Gaëtan Gilbert
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-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-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-24Adapt to fix/cofix changes in Coq (coq/coq#7196)Emilio Jesus Gallego Arias
c.f. https://github.com/coq/coq/pull/7196
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-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-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`.
2018-03-09Fix compilation after the change of API in options.Pierre-Marie Pédrot
2018-03-05[coq] Adapt to correct LTAC module packing coq/coq#6869Emilio Jesus Gallego Arias
2018-03-01[coq] Adapt to coq/coq#6511Emilio Jesus Gallego Arias
coq/coq#6511 contains EConstr-related changes.
2018-03-01[api] Remove some deprecation warnings.Emilio Jesus Gallego Arias
Trivial commit.
2018-02-27Merge remote-tracking branch 'origin/pr/44'Pierre-Marie Pédrot
2018-02-14adapt to Coq#6676Enrico Tassi
2018-02-14[coq] Adapt to coq/coq#6745Emilio Jesus Gallego Arias
Nothing remarkable.
2017-12-26adapt to API.mli removalEnrico Tassi
2017-12-08Adapt to removal of match_appsubterm.Théo Zimmermann
2017-11-24A possible fix after PR#6158 (raw/glob generic printers for ltac values).Hugo Herbelin
Can the printers exploit the ability to now take an environment?
2017-11-21[coq] Adapt to Coq's new functional EXTEND API.Emilio Jesus Gallego Arias
See https://github.com/coq/coq/pull/6197
2017-11-06Generalize the use of repr in Tac2stdlib.Pierre-Marie Pédrot
2017-11-04A possible fix after PR#6047 (a generic printer for ltac values).Hugo Herbelin
2017-11-02Factorizing entries for patterns with type constraints.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:44:57 +0000