aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-21[coq] Adapt to Coq's new functional EXTEND API.Emilio Jesus Gallego Arias
2017-11-06Generalize the use of repr in Tac2stdlib.Pierre-Marie Pédrot
2017-11-04A possible fix after PR#6047 (a generic printer for ltac values).Hugo Herbelin
2017-11-02Factorizing entries for patterns with type constraints.Pierre-Marie Pédrot
2017-11-02Moving pattern type constraints to pattern AST.Pierre-Marie Pédrot
2017-11-02Binding the specialize tactic.Pierre-Marie Pédrot
2017-10-30Put notations in level 5 by default.Pierre-Marie Pédrot
2017-10-30Fix the semantics of introducing with empty intro patterns.Pierre-Marie Pédrot
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 13:51:13 +0000