aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-31 05:24:59 +0000