aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-10-30Fix compilation after merge of Ltac_pretype interface.Pierre-Marie Pédrot
2017-10-27Better printers for toplevel values.Pierre-Marie Pédrot
2017-10-27Adding a command to evaluate Ltac2 expressions.Pierre-Marie Pédrot
2017-10-27Fix goal_matching quotation.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-10-01Using Ltac2 native closures in some tactic APIs.Pierre-Marie Pédrot
2017-10-01Rolling up our own representation of clauses.Pierre-Marie Pédrot
2017-10-01Moving ML types used by Ltac2 to their proper interface.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-26Small language of combinators for lookaheads in parsing.Pierre-Marie Pédrot
2017-09-15Making Ltac2 representation of data coincide with the ML-side one.Pierre-Marie Pédrot
2017-09-15Phantom type for typed closures.Pierre-Marie Pédrot
2017-09-14Abstracting away the type of arities and ML tactics.Pierre-Marie Pédrot
2017-09-14Moving valexpr definition to Tac2ffi.Pierre-Marie Pédrot
2017-09-14Explicit arity for closures.Pierre-Marie Pédrot
2017-09-14Introducing the remember tactic.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-13Better printing for list literals.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-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#27: ... is not a particularly helpful printing of an error mess...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-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-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-06Moving Tac2ffi before Tac2interp.Pierre-Marie Pédrot
2017-09-06Introducing abstract data representations.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-05Binding the firstorder tactic.Pierre-Marie Pédrot
2017-09-05Binding move and intro.Pierre-Marie Pédrot
2017-09-05Introducing quotations for move locations.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 23:55:33 +0000