coq - The formal proof system

Age	Commit message (Expand)	Author
2014-11-10	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot
2014-11-05	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas
2014-11-04	printing/Ppannotation: New annotation for tactic syntactic objects.	Regis-Gianas
2014-11-04	printing/Pptacticsig: New signature for tactic pretty-printers.	Regis-Gianas
2014-11-01	Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.	Arnaud Spiwack
2014-07-27	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot
2014-07-25	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot
2014-04-14	Closing bug #3260	Julien Forest
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-11-10	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot
2013-06-19	Adding genarg printer to debugger.	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-03-14	Pptactic.pr_raw_tactic is now without env argument	letouzey
2012-10-06	Clean-up : removal of Proof_type.tactic_expr	letouzey
2012-10-04	Adding a nominal typing layer to Metasyntax in order to clarify	ppedrot
2012-08-08	Updating headers.	herbelin
2012-05-29	place all pretty-printing files in new dir printing/	letouzey