aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Expand)Author
2016-05-11Making the grammar command extend API purely functional.Pierre-Marie Pédrot
2016-05-11Moving the constr empty entry registering to the state-based API.Pierre-Marie Pédrot
2016-05-11Turning the grammar extend command API into a state-passing one.Pierre-Marie Pédrot
2016-05-11Moving the grammar summary to Pcoq.Pierre-Marie Pédrot
2016-05-10AlistNsep token now accepts an arbitrary separator.Pierre-Marie Pédrot
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Pass user symbol to tactic notation printers.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04Interpretation function can return any untyped value.Pierre-Marie Pédrot
2016-05-04Removing external uses of Val.inject and making Geninterp.interp return Val.tPierre-Marie Pédrot
2016-05-04Removing the Value.of_* API for parameterized types.Pierre-Marie Pédrot
2016-05-04Do not generate generic arguments for data which only requires toplevel values.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Simplifying the code of Tacinterp.Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-02Generate parsing rules for ML tactics in the same order as before a7917a32.Pierre-Marie Pédrot
2016-05-02Useless code in Tacentries.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 06:49:18 +0000