aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/tac2core.ml
AgeCommit message (Expand)Author
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
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-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-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-10-27Rename tac2type -> ltac2_type,Jim Fehrle
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
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-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2019-11-01Add primitive floats to Ltac2Pierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
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-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-25Give a functional type to Ltac1 quotations with a context.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-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-05-10[ltac2] Add primitive integersPierre Roux
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 18:01:43 +0000