aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
AgeCommit message (Expand)Author
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-04-08Merge PR #14093: Register Ltac2 grammar entry as "ltac2" for the Print Gramma...coqbot-app[bot]
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
2021-04-08Merge PR #14027: Print type of offending expression in Ltac2 not-unit warning.coqbot-app[bot]
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
2021-03-29Print type of offending expression in Ltac2 not-unit warning.Pierre-Marie Pédrot
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
2021-03-25Merge PR #13989: fix documentation of Ltac2.Env.expandPierre-Marie Pédrot
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
2021-03-24Merge PR #13973: Factorize goal selector handlingPierre-Marie Pédrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-23fix documentation of Ltac2.Env.expandSamuel Gruetter
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
2021-03-17Merge PR #13938: Fast Ltac2 quoted variable typingcoqbot-app[bot]
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Adding an Ltac2 API to manipulate inductive types.Pierre-Marie Pédrot
2021-03-13Allow scope delimiters in Ltac2 open_constr:(...) quotation.Pierre-Marie Pédrot
2021-03-12Use the new API to prevent retyping of Ltac2 variable quotations.Pierre-Marie Pédrot
2021-03-12Move the responsibility of type-checking to the caller for tactic-in-terms.Pierre-Marie Pédrot
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
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-01-22Add a type of format strings to Ltac2.Pierre-Marie Pédrot
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-11-30Add an abstraction function in the LtacX FFI.Pierre-Marie Pédrot
2020-11-30Store Ltac2 valexpr instead of unevaluated code inside Ltac1 value embedding.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
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-10Add location in existential variable names (CEvar/GEvar).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-11Turn integer into natural in several mlgsPierre Roux
2020-07-18Clarify the Ltac2 invalid identifier message.Pierre-Marie Pédrot
2020-07-18Better location for match! pattern variables in Ltac2.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:52:04 +0000