coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	Continuing 785f82ee1 on reverting not only f5d7b2b1e but also	Hugo Herbelin	2015-01-08
*	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu	2015-01-08
*	Revert "Term: include a function to print terms"	Enrico Tassi	2014-12-27
*	Term: include a function to print terms	Enrico Tassi	2014-12-26
*	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack	2014-12-23
*	Fix compilation error in some configurations.	Arnaud Spiwack	2014-12-23
*	Add a backtracking version of Ltac's [match].	Arnaud Spiwack	2014-12-19
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	Fixed bad newlines in output for std output and emacs.	Pierre Courtieu	2014-12-18
*	msg_info now puts infomsg tag in emacs mode.	Pierre Courtieu	2014-12-16
*	Changed bullet informations to warning for better display in PG.	Pierre Courtieu	2014-12-15
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack	2014-12-12
*	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack	2014-12-12
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Improving error message when one instance-hole is not found.	Hugo Herbelin	2014-12-04
*	Fixing printing of dirpathes in Ppconstr. It was reversed.	Pierre-Marie Pédrot	2014-11-30
*	Adding tag output to references in Ppconstr.	Pierre-Marie Pédrot	2014-11-25
*	Plugging console highlighting in for toplevel and compilation error messages.	Pierre-Marie Pédrot	2014-11-24
*	Removing useless flag of the historical move tactic.	Pierre-Marie Pédrot	2014-11-22
*	Setting printing flags on the printing of mutual inductives.	Pierre-Marie Pédrot	2014-11-20
*	Moving mutual inductive printing from Printer to Printmod.	Pierre-Marie Pédrot	2014-11-20
*	Print [uconstr] in genargs.	Arnaud Spiwack	2014-11-19
*	Proper printer for [uconstr] in [Pptactic].	Arnaud Spiwack	2014-11-19
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	Adding rich-printing facilities to Printmod.	Pierre-Marie Pédrot	2014-11-19
*	Adding notation terminals to coqtop highlight.	Pierre-Marie Pédrot	2014-11-17
*	Fixing semantics of Ppconstr.print_hunks.	Pierre-Marie Pédrot	2014-11-17
*	Missing keywords in Ppconstr.	Pierre-Marie Pédrot	2014-11-17
*	Setting printing tags for Ltac.	Pierre-Marie Pédrot	2014-11-17
*	Moving printing code for red_expr and may_eval to Pptactic.	Pierre-Marie Pédrot	2014-11-17
*	Default styles for printing tags.	Pierre-Marie Pédrot	2014-11-17
*	Setting error tag on generic errors returned by Coqtop.	Pierre-Marie Pédrot	2014-11-17
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Adding tags to messages.	Pierre-Marie Pédrot	2014-11-15
*	Additional style tags for constrs.	Pierre-Marie Pédrot	2014-11-15
*	Setting a keyword tag in Ppconstr.	Pierre-Marie Pédrot	2014-11-15
*	Adding a pretty-printing style library.	Pierre-Marie Pédrot	2014-11-15
*	Move conjugate_verb_to_be next to cString.plural.	Hugo Herbelin	2014-11-13
*	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot	2014-11-10
*	Removing a unused boolean in the TacMove node of tacexpr AST.	Pierre-Marie Pédrot	2014-11-09
*	Removing the legacy intro tactic code.	Pierre-Marie Pédrot	2014-11-07
*	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas	2014-11-05
*	printing/Ppvernac: Fix missing keyword tagging on theorem introducers.	Yann Régis-Gianas	2014-11-05
*	printing/Ppvernac: Fix missing keyword tagging on definition introducers.	Yann Régis-Gianas	2014-11-05
*	printing/Ppvernac: Cosmetics.	Yann Régis-Gianas	2014-11-05
*	printing/Ppannotation: New annotation for tactic syntactic objects.	Regis-Gianas	2014-11-04
*	printing/Pptactic.Make: New.	Regis-Gianas	2014-11-04