aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
AgeCommit message (Expand)Author
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
2017-09-13Adding quotations for the generalize tactic.Pierre-Marie Pédrot
2017-09-09Update backtraces only when the Ltac2 Backtrace flag is set.Pierre-Marie Pédrot
2017-09-09Fix coq/ltac2#26: Ltac1 gives no backtraces.Pierre-Marie Pédrot
2017-09-09Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set.Pierre-Marie Pédrot
2017-09-09Moving Ltac2 backtraces to the Exninfo mechanism.Pierre-Marie Pédrot
2017-09-09Fix coq/ltac2#25: Control.case should not be able to catch Control.throw.Pierre-Marie Pédrot
2017-09-08Using a dedicated argument for tactic quotations.Pierre-Marie Pédrot
2017-09-08Fix coq/ltac2#24: There should be a way to turn an exn into a message.Pierre-Marie Pédrot
2017-09-07Communicate the backtrace through the monad.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 11:14:43 +0000