aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrparser.mlg
AgeCommit message (Expand)Author
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
2021-03-31Fix printing of ssr do intros and seq tacticsLasse Blaauwbroek
2020-12-27Make ssrtermkind algebraic instead of a charLasse Blaauwbroek
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-22Fix printing of wit_constr and some ssr problems with printing empty listsLasse Blaauwbroek
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-03Wrap ssr tactics into V82.tactic.Pierre-Marie Pédrot
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the s...Pierre Roux
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-01Refactor lookaheads using DSLMaxime Dénès
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-26Remove unused grammar productionsJim Fehrle
2019-07-23Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-05Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTENDPierre-Marie Pédrot
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-03Apparently unused ssr nonterminalsJim Fehrle
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
2019-04-23[ssr] set under's tactic argument at LEVEL 3Erik Martin-Dorel
2019-04-23[ssr] under: Fix the defective form ("=> [*|*]" implied) and its docErik Martin-Dorel
2019-04-23[ssr] new syntax for the under tacticEnrico Tassi
2019-04-23[ssr] under: Add support for one-liners "under (…) by [tac1|tac2]."Erik Martin-Dorel
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-04-02[ssr] implement "under i: ext_lemma" by rewrite ruleEnrico Tassi
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-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-01-21[ssr] cleanup of some commentsEnrico Tassi
2019-01-18[ssr] clean up implementation of {}/v -> /v{v}Enrico Tassi
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-11-28Merge PR #9070: [ssreflect] Export more parsing witnesses.Enrico Tassi
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-26[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:35:56 +0000