aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-29Removing dead code for handling of array litterals.Pierre-Marie Pédrot
2017-08-29Factorizing code for declaration of primitive tactics.Pierre-Marie Pédrot
2017-08-29Implementing Ltac2 antiquotations in constr syntax.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-28Fix README.Pierre-Marie Pédrot
2017-08-28Fix coq/ltac2#6: Expected and actual types are flipped.Pierre-Marie Pédrot
2017-08-28typosgallais
2017-08-27Do not reuse the Val.t type in toplevel values.Pierre-Marie Pédrot
2017-08-27Notation for clear.Pierre-Marie Pédrot
2017-08-27Fix semantics of the solve tactical.Pierre-Marie Pédrot
2017-08-27Ensure no confusion with unit in rigid variables.Pierre-Marie Pédrot
2017-08-27Proper handling of rigid variables in subtyping.Pierre-Marie Pédrot
2017-08-27Introducing rebindable toplevel definitions.Pierre-Marie Pédrot
2017-08-26Allowing calls to Ltac2 inside Ltac1.Pierre-Marie Pédrot
2017-08-26TyposHugo Herbelin
2017-08-26Allowing to insert calls to Ltac1 references in Ltac2.Pierre-Marie Pédrot
2017-08-25Adding more notations for the lulz.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-25More bindings to primitive tactics.Pierre-Marie Pédrot
2017-08-25Respect the default goal selector in toplevel invocations.Pierre-Marie Pédrot
2017-08-25Parse specifically idents as destruction arguments.Pierre-Marie Pédrot
2017-08-25Lookahead to cheat the constr parser in order to parse "& IDENT".Pierre-Marie Pédrot
2017-08-24Fix the semantics of fail, as it should enter the goal.Pierre-Marie Pédrot
2017-08-24Documentation about the transition from Ltac1.Pierre-Marie Pédrot
2017-08-24Removing dead code about arrays in the AST.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 for the unfold tactic.Pierre-Marie Pédrot
2017-08-24Adding a notation scope for global references.Pierre-Marie Pédrot
2017-08-24Adding notation for the remaining reduction functions.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
2017-08-24Use references in reduction tactics.Pierre-Marie Pédrot
2017-08-18More precise type for quotation entries.Pierre-Marie Pédrot
2017-08-18Removing dead code.Pierre-Marie Pédrot
2017-08-18Laxer dependencies between file and link reordering.Pierre-Marie Pédrot
2017-08-18Notations for a few reduction functions.Pierre-Marie Pédrot
2017-08-18Exporting scopes for occurrences.Pierre-Marie Pédrot
2017-08-18Trying to enhance the printing of tactic expressions.Pierre-Marie Pédrot
2017-08-11Introducing a syntax for goal dispatch.Pierre-Marie Pédrot
2017-08-08Another batch of primitive operations.Pierre-Marie Pédrot
2017-08-08Code simplification in quotations.Pierre-Marie Pédrot
2017-08-07Defining several aliases for built-in tactics.Pierre-Marie Pédrot
2017-08-07Defining abbreviations for tactics that can parse as atoms.Pierre-Marie Pédrot
2017-08-07Fix location of not-unit warning.Pierre-Marie Pédrot
2017-08-07Fix parsing of parenthesized expressions.Pierre-Marie Pédrot
2017-08-07Defining a few base tacticals.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 22:38:53 +0000