coq - The formal proof system

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