aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/g_ltac2.mlg
AgeCommit message (Expand)Author
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-10Allow to register deprecation status in Ltac2 term and notation declarations.Pierre-Marie Pédrot
2021-03-10Allow the presence of type casts for return values in Ltac2.Pierre-Marie Pédrot
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-11-04Adding an if-then-else syntax to Ltac2.Pierre-Marie Pédrot
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Ltac2: use ComTactic infrastructureGaëtan Gilbert
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-07-01Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.Pierre-Marie Pédrot
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-04-12Tweak grammar to make doc_grammar happyJim Fehrle
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-03-01Move lookahead combinators to PcoqMaxime Dénès
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
2020-02-24Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.Tej Chajed
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2020-02-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-07-29Fix #10088: Incompatibility with ssreflect's ampersand syntactic sugar.Pierre-Marie Pédrot
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-06-25Adding the ability to transfer Ltac2 variables to Ltac1 quotations.Pierre-Marie Pédrot
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:20:27 +0000