coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	printing/Pptacticsig: New signature for tactic pretty-printers.	Regis-Gianas	2014-11-04
*	lib/Ppconstr: Cosmetics.	Regis-Gianas	2014-11-04
*	Rebase artefact.	Regis-Gianas	2014-11-04
*	lib/Pp.tag: New.	Regis-Gianas	2014-11-04
*	printing/Ppannotation: Introduce a new annotation for keywords.	Regis-Gianas	2014-11-04
*	printing/richPrinter: Fix incorrect signatures.	Regis-Gianas	2014-11-04
*	printing/RichPrinter: New API for rich pretty-printing.	Regis-Gianas	2014-11-04
*	Ppvernac: Publish new rich pretty-printer.	Regis-Gianas	2014-11-04
*	Ppannotation.t: New constructor AVernac.	Regis-Gianas	2014-11-04
*	Ppvernacsig: New.	Regis-Gianas	2014-11-04
*	Ppvernac.Make: New	Regis-Gianas	2014-11-04