aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Gravatar Hugo Herbelin2016-04-27
* Revert "Using existing names as a basis for the inner names of the pattern-ma...Gravatar Hugo Herbelin2016-04-27
* Revert "Vers un filtrage profond ..."Gravatar Hugo Herbelin2016-04-27
* Vers un filtrage profond ...Gravatar Hugo Herbelin2016-04-27
* Using existing names as a basis for the inner names of the pattern-matching p...Gravatar Hugo Herbelin2016-04-27
* Fixing a De Bruijn bug in computing return predicate by inversion.Gravatar Hugo Herbelin2016-04-27
* Add support for deep dependencies in variables within the recursive structure.Gravatar Hugo Herbelin2016-04-27
* Add support for generalization also on named variables in pattern-matchingGravatar Hugo Herbelin2016-04-27
* More abstraction in cases.mli.Gravatar Hugo Herbelin2016-04-27
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* Revert "Re-add -beautify by default."Gravatar Hugo Herbelin2016-04-27
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
* Typo in comment.Gravatar Hugo Herbelin2016-04-27
* Fixing space in an error message.Gravatar Hugo Herbelin2016-04-27
* Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
* When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
* Re-add -beautify by default.Gravatar Hugo Herbelin2016-04-27
* Add plugins to Makefile.Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in front of terminal in printing vernac.Gravatar Hugo Herbelin2016-04-27
* Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
* Temporary hack to restore missing printing of "constr:" in right-handGravatar Hugo Herbelin2016-04-27
* Temporary hack to compensate missing comma while re-printing tacticGravatar 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
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 08:09:18 +0000