aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Expand)Author
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Hugo Herbelin
2016-04-27Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Hugo Herbelin
2016-04-27Revert "Fixing Add Parametric Relation by adding printer for binders."Hugo Herbelin
2016-04-27Revert "Fixing printing of Register retroknowledge."Hugo Herbelin
2016-04-27Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Hugo Herbelin
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
2016-04-27Revert "Fixing space in an error message."Hugo Herbelin
2016-04-27Revert "Typo in comment."Hugo Herbelin
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Typo in comment.Hugo Herbelin
2016-04-27Fixing space in an error message.Hugo Herbelin
2016-04-27When interpreting "match goal with ... end" in ltac, expand evars byHugo Herbelin
2016-04-27Passing around the precedence to the generic printer so as to solveHugo Herbelin
2016-04-27A fix to #3709: ensuring extra parentheses when a tactic entry has aHugo Herbelin
2016-04-27Fixing printing of Register retroknowledge.Hugo Herbelin
2016-04-27Fixing Add Parametric Relation by adding printer for binders.Hugo Herbelin
2016-04-27Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
2016-04-27Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-25Factorizing code in tactic notations.Pierre-Marie Pédrot
2016-04-25Documenting API.Pierre-Marie Pédrot
2016-04-24Remove dead registering code in Pcoq.Pierre-Marie Pédrot
2016-04-24Disentangle tactic notation resolution from Pcoq.Pierre-Marie Pédrot
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-24Factorizing the declaration of ML notation printing in Tacentries.Pierre-Marie Pédrot
2016-04-15Merge remote-tracking branch 'OFFICIAL/trunk' into morefreshPierre Courtieu
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-12Adding toplevel representation sharing for some generic arguments.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Hugo Herbelin
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
2016-03-31Moving the code handling tactic notations to Tacentries.Pierre-Marie Pédrot
2016-03-31Moving the Tactic Notation entry parser from Pcoq to Tacentries.Pierre-Marie Pédrot
2016-03-28Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-03-28Fixing an evar leak in Rewrite introduced by 968dfdb15.Pierre-Marie Pédrot
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Making Eqdecide independent of Extratactics.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:27:18 +0000