aboutsummaryrefslogtreecommitdiff
path: root/src/tac2core.ml
AgeCommit message (Expand)Author
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
2017-09-06Fix coq/ltac2#23: Int.compare should not be uniformly 0.Pierre-Marie Pédrot
2017-09-06Using higher-order representation for closures.Pierre-Marie Pédrot
2017-09-06Parameterizing over parameters in ML functions from Tac2core.Pierre-Marie Pédrot
2017-09-06The interp_app function now takes a closure as an argument.Pierre-Marie Pédrot
2017-09-06Code factorization.Pierre-Marie Pédrot
2017-09-05Refine does not evar-normalizes the goal preemptively.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-04More precise error messages for scope failure.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-04Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining.Pierre-Marie Pédrot
2017-09-04Implementing lazy matching over terms.Pierre-Marie Pédrot
2017-09-03Introducing a macro for constr matching.Pierre-Marie Pédrot
2017-09-03Moving generic arguments to Tac2quote.Pierre-Marie Pédrot
2017-09-03Uniform handling of locations in the various AST.Pierre-Marie Pédrot
2017-09-03Allowing ML objects to return mere tactic expressions.Pierre-Marie Pédrot
2017-09-03Allowing complex types in ML objects.Pierre-Marie Pédrot
2017-09-03Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies.Pierre-Marie Pédrot
2017-08-31Expand the primitive functions on terms.Pierre-Marie Pédrot
2017-08-29Fix printing of Ltac2 in quotations.Pierre-Marie Pédrot
2017-08-29Fixing printing of tactic expressions.Pierre-Marie Pédrot
2017-08-29Rolling our own generic arguments.Pierre-Marie Pédrot
2017-08-29Rolling our own dynamic types for Ltac2.Pierre-Marie Pédrot
2017-08-29Pass Ltac2 variables in a dedicated environment for generic arguments.Pierre-Marie Pédrot
2017-08-29Factorizing code for declaration of primitive tactics.Pierre-Marie Pédrot
2017-08-29Binding an unsafe substitution function.Pierre-Marie Pédrot
2017-08-29Binding primitives to generate fresh variables.Pierre-Marie Pédrot
2017-08-27Do not reuse the Val.t type in toplevel values.Pierre-Marie Pédrot
2017-08-26Allowing calls to Ltac2 inside Ltac1.Pierre-Marie Pédrot
2017-08-26Allowing to insert calls to Ltac1 references in Ltac2.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-25Do not return STRING scopes in the tuple produced by "seq" scopes.Pierre-Marie Pédrot
2017-08-24Rely on quoting for lists instead of hardwiring it in the AST.Pierre-Marie Pédrot
2017-08-24Adding a notation scope for global references.Pierre-Marie Pédrot
2017-08-24Fix typing of reference quotations.Pierre-Marie Pédrot
2017-08-24Adding a scope for reduction flags.Pierre-Marie Pédrot
2017-08-24Introducing a quotation for global references.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 13:52:36 +0000