aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Function.Gravatar Hugo Herbelin2016-04-27
* Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-04-27
* Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-04-27
* Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-04-27
* Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Arguments.Gravatar Hugo Herbelin2016-04-27
* Printing notations as parsed.Gravatar Hugo Herbelin2016-04-27
* Revert "Protect printing of intro-patterns from collision when "[|" orGravatar Hugo Herbelin2016-04-27
* Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-04-27
* Protect printing of intro-patterns from collision when "[|" or "|]"Gravatar Hugo Herbelin2016-04-27
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-04-27
* Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of inversion as.Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-04-27
* Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
* In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Gravatar Hugo Herbelin2016-04-27
* Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-04-27
* Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* Temporary deactivate re-interpretation of terms in beautify.Gravatar Hugo Herbelin2016-04-27
* Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-04-27
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Changing rule for "*" in Operator_Properties so that, iterated, itGravatar Hugo Herbelin2016-04-27
* Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-04-27
* So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-04-27
* Adding a target check-beautify for testing reparsability ofGravatar Hugo Herbelin2016-04-27
* Adding a target for beautification.Gravatar Hugo Herbelin2016-04-27
* Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-04-27
* A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
* Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
* Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-04-25
* Simplifying and uniformizing the implementation of tactic notations.Gravatar Pierre-Marie Pédrot2016-04-25
|\
| * Removing dead code related to printing of ML tactics in Pptactic.Gravatar Pierre-Marie Pédrot2016-04-25
| * 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
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\
| * Fixing output test Notations2.Gravatar Hugo Herbelin2016-04-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 00:27:45 +0000