coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-14	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-03-02	Noise for nothing	pboutill
2012-02-20	Correct application of head reduction.	msozeau
2012-02-15	Avoid unnecessary normalizations w.r.t. evars in Program.	msozeau
2012-02-14	- Fix dependency computation in eterm to not consider filtered variables.	msozeau
2011-10-18	Fix inductive coercion code in Program (bug #2378)	msozeau
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2011-03-05	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-10-31	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-30	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau
2010-06-30	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-05-19	Remove compile-command pragmas for emacs	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-01-14	- Show Obligation Tactic	msozeau
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-07	Fixes in Program:	msozeau
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey