coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Printmod: handle more examples thanks to better nametab use	letouzey	2013-03-21
*	Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)	letouzey	2013-03-21
*	Declaremods: a few syntactic improvements	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey	2013-03-13
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of mod_bound_id	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	Fixing bug #2809 (anomaly when printing a module with notations due to	herbelin	2012-06-20
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29