aboutsummaryrefslogtreecommitdiff
path: root/test-suite/ltac2
AgeCommit message (Expand)Author
2021-04-08remove `with hintdb` variant of Ltac2 `unify`, becauseSamuel Gruetter
2021-04-07unify for Ltac2Samuel Gruetter
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Add tests for the new Ltac2 Ind API.Pierre-Marie Pédrot
2021-03-10Adding a parsing test.Pierre-Marie Pédrot
2021-01-22Add tests for the printf feature.Pierre-Marie Pédrot
2020-11-30Add test for this new function.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-01Add a test for Ltac2 parsing of parameterized types.Pierre-Marie Pédrot
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-11More tests of rebinding Ltac2 definitionsKenji Maillard
2020-05-11Correcting ltac2's documentation on values turning test into proper check.Kenji Maillard
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
2020-03-03Ltac2: Add notation for enough and eenoughMichael Soegtrop
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
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-09-24Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindGaëtan Gilbert
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-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
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 09:51:45 +0000