coq - The formal proof system

Age	Commit message (Expand)	Author
2016-04-27	Revert "Not taking arguments given by name or position into account when"	Hugo Herbelin
2016-04-27	Revert "Adding a target for beautification."	Hugo Herbelin
2016-04-27	Revert "Adding a target check-beautify for testing reparsability of"	Hugo Herbelin
2016-04-27	Revert "So as to beautify to work, do not use notations in Inductive types"	Hugo Herbelin
2016-04-27	Revert "Protect the beautifier from change in the lexer state (typically by"	Hugo Herbelin
2016-04-27	Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"	Hugo Herbelin
2016-04-27	Revert "In the short term, stronger invariant on the syntax of TacAssert, what"	Hugo Herbelin
2016-04-27	Revert "Being defensive in printing implicit arguments also with manual"	Hugo Herbelin
2016-04-27	Revert "Temporary deactivate re-interpretation of terms in beautify."	Hugo Herbelin
2016-04-27	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin
2016-04-27	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin
2016-04-27	Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...	Hugo Herbelin
2016-04-27	Revert "Fixing printers for pr_auto_using and pr_firstorder_using."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of pat%constr."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of induction/destruct as."	Hugo Herbelin
2016-04-27	Revert "Fixing extra space in printing destruct/induction as."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of inversion as."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of keeping hyp on the fly."	Hugo Herbelin
2016-04-27	Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"	Hugo Herbelin
2016-04-27	Revert "Protect printing of intro-patterns from collision when "[\|" or "\|]""	Hugo Herbelin
2016-04-27	Revert "Protect printing of ltac's "context [...]" from possible collision"	Hugo Herbelin
2016-04-27	Revert "Revert "Protect printing of intro-patterns from collision when "[\|" or"	Hugo Herbelin
2016-04-27	Revert "Printing notations as parsed."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of Arguments."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of Polymorphic/Monomorphic."	Hugo Herbelin
2016-04-27	Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of Instance."	Hugo Herbelin
2016-04-27	Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."	Hugo Herbelin
2016-04-27	Revert "Fixing extra space in printing bullets."	Hugo Herbelin
2016-04-27	Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...	Hugo Herbelin
2016-04-27	Revert "Simplification in ppvernac.ml."	Hugo Herbelin
2016-04-27	Revert "Isolating and exporting a function for printing body of a recursive d...	Hugo Herbelin
2016-04-27	Revert "Fixing printing of Function."	Hugo Herbelin
2016-04-27	Revert "Adding printers for ring and field commands."	Hugo Herbelin
2016-04-27	Revert "Fixing Add Parametric Relation by adding printer for binders."	Hugo Herbelin
2016-04-27	Revert "Fixing printing of Register retroknowledge."	Hugo Herbelin
2016-04-27	Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"	Hugo Herbelin
2016-04-27	Revert "Passing around the precedence to the generic printer so as to solve"	Hugo Herbelin
2016-04-27	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin
2016-04-27	Revert "Temporary hack to restore missing printing of "constr:" in right-hand"	Hugo Herbelin
2016-04-27	Revert "Taking into account the original grammar rule to print generic"	Hugo Herbelin
2016-04-27	Revert "Fixing extra space in front of terminal in printing vernac."	Hugo Herbelin
2016-04-27	Revert "Add plugins to Makefile."	Hugo Herbelin
2016-04-27	Revert "Re-add -beautify by default."	Hugo Herbelin
2016-04-27	Revert "When interpreting "match goal with ... end" in ltac, expand evars by"	Hugo Herbelin
2016-04-27	Revert "Warn about possible shadowing of a name occurring in a "in" clause."	Hugo Herbelin
2016-04-27	Revert "Fixing space in an error message."	Hugo Herbelin
2016-04-27	Revert "Typo in comment."	Hugo Herbelin
2016-04-27	Revert "Fixing a mispelling coma -> comma."	Hugo Herbelin
2016-04-27	Revert "Revert "Re-add -beautify by default.""	Hugo Herbelin