aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
* Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
* Removing the Value.of_* API for parameterized types.Gravatar Pierre-Marie Pédrot2016-05-04
* Do not generate generic arguments for data which only requires toplevel values.Gravatar Pierre-Marie Pédrot2016-05-04
* More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Simplifying the code of Tacinterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* Generate parsing rules for ML tactics in the same order as before a7917a32.Gravatar Pierre-Marie Pédrot2016-05-02
* Useless code in Tacentries.Gravatar Pierre-Marie Pédrot2016-05-02
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing Add Parametric Relation by adding printer for binders."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Register retroknowledge."Gravatar Hugo Herbelin2016-04-27
* Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Gravatar Hugo Herbelin2016-04-27
* Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
* Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing space in an error message."Gravatar Hugo Herbelin2016-04-27
* Revert "Typo in comment."Gravatar Hugo Herbelin2016-04-27
* Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* Typo in comment.Gravatar Hugo Herbelin2016-04-27
* Fixing space in an error message.Gravatar Hugo Herbelin2016-04-27
* When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
* Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
* A fix to #3709: ensuring extra parentheses when a tactic entry has aGravatar Hugo Herbelin2016-04-27
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-04-27
* Fixing Add Parametric Relation by adding printer for binders.Gravatar Hugo Herbelin2016-04-27
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-04-27
* Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
* Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
* Factorizing code in tactic notations.Gravatar Pierre-Marie Pédrot2016-04-25
* Documenting API.Gravatar Pierre-Marie Pédrot2016-04-25
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Disentangle tactic notation resolution from Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Factorizing the declaration of ML notation printing in Tacentries.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Adding toplevel representation sharing for some generic arguments.Gravatar Pierre-Marie Pédrot2016-04-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 17:24:17 +0000