coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	Continue killing hidden tactics : no more generated h_xxx	letouzey	2012-10-15
*	Stylistic improvement: avoid a "if match List.hd"	letouzey	2012-10-15
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	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
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Made Pp.std_ppcmds opaque.	ppedrot	2012-09-13
*	Updating headers.	herbelin	2012-08-08
*	Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)	letouzey	2012-07-12
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	More cleaning	ppedrot	2012-06-01
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29