aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)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
Fix for https://github.com/coq/coq/pull/8984
2019-03-31[coq] Adapt to coq/coq#9815Pierre Roux
2019-03-31overlay for PR 9733Enrico Tassi
2019-03-29[dune] Full Dune support.Emilio Jesus Gallego Arias
This add experimental support for building the full Ltac2 plugin with Dune, see tree at https://github.com/ejgallego/dune/tree/coq
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-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
Adapt to coq/coq#8817 (SProp)
2019-02-20[coq] Fix OCaml warnings.Emilio Jesus Gallego Arias
In anticipation to https://github.com/coq/coq/pull/9605 , we fix all OCaml warnings. Fixes coq/ltac2#107
2019-02-14Adapt to coq/coq#8817 (SProp)Gaëtan Gilbert
2019-02-09[coq] Adapt to coq/coq#9137Emilio Jesus Gallego Arias
To be merged when the upstream PR is merged. Not sure this is the right thing to do tho.
2019-02-08Remove VtUnknown classificationMaxime Dénès
That classification is going to disappear from Coq. However, I don't understand why it was used here. Can you confirm that the command can not open a proof?
2019-02-01Adapt to https://github.com/coq/coq/pull/9410Maxime Dénès
2019-01-17Adapt to Coq's new proof mode APIMaxime Dénès
2018-12-10[coq] Adapt to coq/coq#9172Emilio Jesus Gallego Arias
Note that this highlights some issues with the current Coq interface, not clear what should we do.
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-17[coq] Overlay to adapt to coq/coq#9003Emilio Jesus Gallego Arias
To be merged when the Coq developers merge the PR upstream.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-25 22:39:13 +0000