aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/g_tactic.mlg
AgeCommit message (Expand)Author
2019-04-29Exposing a change_no_check tactic.Hugo Herbelin
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-04-02Rename the INT token to NUMERALPierre Roux
2019-04-01Replace type sign = bool with SPlus | SMinusPierre Roux
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-11-17[ltac] Use CAst nodes in the tactic AST.Emilio Jesus Gallego Arias
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-06-29Port g_tactic to the homebrew GEXTEND parser.Pierre-Marie Pédrot