aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | | | Revert "Protect the beautifier from change in the lexer state (typically by"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Being defensive in printing implicit arguments also with manual"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Temporary deactivate re-interpretation of terms in beautify."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of pat%constr."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of induction/destruct as."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing extra space in printing destruct/induction as."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of inversion as."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of keeping hyp on the fly."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 "Protect printing of intro-patterns from collision when "[|" or "|]""Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Protect printing of ltac's "context [...]" from possible collision"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Printing notations as parsed."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of Arguments."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of Polymorphic/Monomorphic."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of Instance."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing extra space in printing bullets."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Simplification in ppvernac.ml."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Isolating and exporting a function for printing body of a recursive d...Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of Function."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Adding printers for ring and field commands."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 "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Taking into account the original grammar rule to print generic"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing extra space in front of terminal in printing vernac."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Add plugins to Makefile."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Re-add -beautify by default."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Warn about possible shadowing of a name occurring in a "in" clause."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 "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Revert "Re-add -beautify by default.""Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* | | | Revert "More abstraction in cases.mli."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Add support for generalization also on named variables in pattern-mat...Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Add support for deep dependencies in variables within the recursive s...Gravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 20:06:03 +0000