aboutsummaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-09-05More static invariants for typeclass_eauto.Pierre-Marie Pédrot
2017-09-05ML bindings of 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-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-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-04Proper anomalies for missing registered primitives.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-09-02Fix coq/ltac2#12: Error should name which match cases are unhandled.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-31Properly handling internal errors from Coq.Pierre-Marie Pédrot
2017-08-31Expand the primitive functions on terms.Pierre-Marie Pédrot
2017-08-31Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Requi...Pierre-Marie Pédrot
2017-08-31Fix coq/ltac2#3: Constructor expects n arguments should name which constructo...Pierre-Marie Pédrot
2017-08-30Binding reduction functions acting 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-29Centralizing tag declarations.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-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 coq/ltac2#6: Expected and actual types are flipped.Pierre-Marie Pédrot
2017-08-27Do not reuse the Val.t type in toplevel values.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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 04:52:51 +0000