aboutsummaryrefslogtreecommitdiff
path: root/ltac/g_auto.ml4
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
2016-06-16Typeclasses eauto based on new proof engine,Matthieu Sozeau
2016-04-27Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Hugo Herbelin
2016-04-27Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 09:43:44 +0000