aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
AgeCommit message (Expand)Author
2019-04-09Adapt to Coq's PR #9909Maxime Dénès
2019-03-31[coq] Adapt to coq/coq#9815Pierre Roux
2019-03-31overlay for PR 9733Enrico Tassi
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
2019-02-20[coq] Fix OCaml warnings.Emilio Jesus Gallego Arias
2019-02-14Adapt to coq/coq#8817 (SProp)Gaëtan Gilbert
2019-02-01Adapt to https://github.com/coq/coq/pull/9410Maxime Dénès
2018-12-10[coq] Adapt to coq/coq#9172Emilio Jesus Gallego Arias
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-15Fix compilation w.r.t. coq/coq#8779.Pierre-Marie Pédrot
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
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-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-28Fix w.r.t. coq/coq#7521.Pierre-Marie Pédrot
2018-04-11Fix compilation w.r.t. coq/coq#7213.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
2018-03-10[coq] Adapt to coq/coq#6837.Emilio Jesus Gallego Arias
2018-03-10[coq] Adapt to coq/coq#6831.Emilio Jesus Gallego Arias
2018-03-05[coq] Adapt to correct LTAC module packing coq/coq#6869Emilio Jesus Gallego Arias
2018-03-01[api] Remove some deprecation warnings.Emilio Jesus Gallego Arias
2018-02-14adapt to Coq#6676Enrico Tassi
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
2017-11-04A possible fix after PR#6047 (a generic printer for ltac values).Hugo Herbelin
2017-10-30Introducing the change tactic.Pierre-Marie Pédrot
2017-10-30Fix compilation after merge of Ltac_pretype interface.Pierre-Marie Pédrot
2017-10-27Fix relative meaning of Pattern vs. Context in match goal.Pierre-Marie Pédrot
2017-10-27Stubs for goal matching: quotation and matching function.Pierre-Marie Pédrot
2017-10-07Implementing the Constr.in_context function.Pierre-Marie Pédrot
2017-10-07Remove unused warnings.Pierre-Marie Pédrot
2017-10-07Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.Pierre-Marie Pédrot
2017-10-01Abstracting away the implementation of value representations.Pierre-Marie Pédrot
2017-09-30Abstracting away the primitive functions on valexpr datatype.Pierre-Marie Pédrot
2017-09-26Adding quotations for the assert family of tactics.Pierre-Marie Pédrot
2017-09-14Abstracting away the type of arities and ML tactics.Pierre-Marie Pédrot
2017-09-14Explicit arity for closures.Pierre-Marie Pédrot
2017-09-14Binding the pose/set family of tactics.Pierre-Marie Pédrot
2017-09-14Use a simpler syntax for generalize grammar.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 17:31:03 +0000