aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/g_tactic.mlg
AgeCommit message (Expand)Author
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-17Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.Hugo Herbelin
2020-11-16Suggesting to use injection when an injection pattern is given to destruct.Hugo Herbelin
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is de...Hugo Herbelin
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-10-18factorize or_var_mapAlexandre Moine
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:07:46 +0000