aboutsummaryrefslogtreecommitdiff
path: root/src/tac2entries.ml
AgeCommit message (Expand)Author
2018-07-23Fix deprecated warnings from Pcoq.Pierre-Marie Pédrot
2018-06-18Adapt to Coq's PR #7797 (removal of reference).Maxime Dénès
2018-06-18Fixing a batch of deprecation warnings.Pierre-Marie Pédrot
2018-05-25Renaming smartmap and fold_map according to Coq PR #7177.Hugo Herbelin
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-09Fix compilation after the change of API in options.Pierre-Marie Pédrot
2018-03-01[coq] Adapt to coq/coq#6511Emilio Jesus Gallego Arias
2017-11-02Moving pattern type constraints to pattern AST.Pierre-Marie Pédrot
2017-10-30Put notations in level 5 by default.Pierre-Marie Pédrot
2017-10-30Introducing the change tactic.Pierre-Marie Pédrot
2017-10-27Adding a command to evaluate Ltac2 expressions.Pierre-Marie Pédrot
2017-10-27Stubs for goal matching: quotation and matching function.Pierre-Marie Pédrot
2017-10-07Remove unused warnings.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-14Moving valexpr definition to Tac2ffi.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-09If backtrace is missing, don't print it.Pierre-Marie Pédrot
2017-09-09Moving Ltac2 backtraces to the Exninfo mechanism.Pierre-Marie Pédrot
2017-09-08Fix coq/ltac2#22: Argument to Tactic_failure should be printed.Pierre-Marie Pédrot
2017-09-07Slightly better printing for anonymous closures.Pierre-Marie Pédrot
2017-09-07Fix coq/ltac2#21: Backtraces should print Ltac2 closures.Pierre-Marie Pédrot
2017-09-07Communicate the backtrace through the monad.Pierre-Marie Pédrot
2017-09-06Using higher-order representation for closures.Pierre-Marie Pédrot
2017-09-05Introducing quotations for move locations.Pierre-Marie Pédrot
2017-09-05Quotations for auto-related tactics.Pierre-Marie Pédrot
2017-09-04More notations for primitive tactics.Pierre-Marie Pédrot
2017-09-04Implementing the non-strict mode.Pierre-Marie Pédrot
2017-09-04Better backtraces for a few datatypes.Pierre-Marie Pédrot
2017-09-04Quick-and-dirty backtrace mechanism for the interpreter.Pierre-Marie Pédrot
2017-09-04Closures now wear the constant they originated from.Pierre-Marie Pédrot
2017-09-03Introducing a macro for constr matching.Pierre-Marie Pédrot
2017-09-03Uniform handling of locations in the various AST.Pierre-Marie Pédrot
2017-09-02Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.Pierre-Marie Pédrot
2017-09-01Ensuring the Ltac definitions have lowercase names.Pierre-Marie Pédrot
2017-08-31Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Requi...Pierre-Marie Pédrot
2017-08-27Introducing rebindable toplevel definitions.Pierre-Marie Pédrot
2017-08-25Introducing a distinct bindings scope.Pierre-Marie Pédrot
2017-08-25Renaming the bindings scope into with_bindings.Pierre-Marie Pédrot
2017-08-25Respect the default goal selector in toplevel invocations.Pierre-Marie Pédrot
2017-08-24Adding a notation scope for global references.Pierre-Marie Pédrot
2017-08-24Adding a scope for reduction flags.Pierre-Marie Pédrot
2017-08-18Exporting scopes for occurrences.Pierre-Marie Pédrot
2017-08-11Introducing a syntax for goal dispatch.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.Pierre-Marie Pédrot
2017-08-05Exporting the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Introducing quotations for the rewrite tactic.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:17:35 +0000