coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Pass user symbol to tactic notation printers.	Pierre-Marie Pédrot	2016-05-08
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Revert "Taking into account the original grammar rule to print generic"	Hugo Herbelin	2016-04-27
*	Taking into account the original grammar rule to print generic	Hugo Herbelin	2016-04-27
*	Removing dead code related to printing of ML tactics in Pptactic.	Pierre-Marie Pédrot	2016-04-25
*	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Tactic notation printing accesses all the token data.	Pierre-Marie Pédrot	2016-01-16
\| *	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-13
* \|	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-10
\|\\|
\| *	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
* \|	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot	2015-01-23
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot	2014-11-10
*	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas	2014-11-05
*	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-04
*	Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.	Arnaud Spiwack	2014-11-01
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot	2014-07-25
*	Closing bug #3260	Julien Forest	2014-04-14
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Adding genarg printer to debugger.	ppedrot	2013-06-19
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	Pptactic.pr_raw_tactic is now without env argument	letouzey	2013-03-14
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Adding a nominal typing layer to Metasyntax in order to clarify	ppedrot	2012-10-04
*	Updating headers.	herbelin	2012-08-08
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29