aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
AgeCommit message (Expand)Author
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
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
2020-07-01Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.Pierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-11Generalize the Ltac2 value criterion to pure let-bindings.Pierre-Marie Pédrot
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-05-03Ensure eintros allows creating evarsPaolo G. Giarrusso
2020-04-23Merge PR #12083: Tweak ltac2 grammar to make doc_grammar happyPierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-12Tweak grammar to make doc_grammar happyJim Fehrle
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-04-03Adding fresh-in-context: a short form of Ltac2 Fresh.fresh.Hugo Herbelin
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio 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-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
2020-03-18Hide the Ltac2 binder type.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Merge PR #11578: [exn] Keep information from multiple extra exn handlersPierre-Marie Pédrot
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
2020-03-03[exn] Keep information from multiple extra exn handlersEmilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-03-03Ltac2: Add notation for enough and eenoughMichael Soegtrop
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:38:17 +0000