aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:50:49 +0000