coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-25	Tacinterp: fewer use of old-style goals.	Arnaud Spiwack
2013-07-05	Removing SortArgType.	ppedrot
2013-07-05	Expurgating the useless difference between List0 and List1 at the	ppedrot
2013-07-02	Removed the ad-hod handling of wit_tacticn.	ppedrot
2013-06-30	Fixing Camlp4 compilation.	ppedrot
2013-06-27	Getting rid of IntroPatternArgType.	ppedrot
2013-06-21	Splitted up Genarg in four different levels:	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-19	Fixing argument extension. Instead of qualified names, string	ppedrot
2013-06-18	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot
2013-06-18	Removing the various glob/subst/interp registering functions for	ppedrot
2013-06-12	Added Genarg as generic argument type.	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey
2013-03-05	More monomorphization.	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-16	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey
2012-10-04	Moved Compat to parsing. This permits to break the dependency of the	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-10-02	Argextend: avoid useless "open Extrawit"	letouzey
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey