coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Catch NotArity exception and transform it into an anomaly in retyping.	msozeau	2011-04-11
*	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin	2011-04-08
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	A few extra combinators about rel_declaration/named_declaration + a bit of doc	herbelin	2011-04-06
*	As remarked by Enrico, we'd better use eq_constr than structural equality	herbelin	2011-03-31
*	- Remove useless grammar rule	msozeau	2011-03-23
*	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau	2011-03-23
*	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau	2011-03-13
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau	2011-03-10
*	Do not forget conv_pbs when resetting an evm:	msozeau	2011-03-10
*	Solve evar instantiations in the right environment.	msozeau	2011-03-08
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Revert commit r13883: instantiating ?n by a lambda when "?n a" has to	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	A few more betaiota on environments and types of error messages. Seems to	herbelin	2011-03-05
*	Added support for instantiation of ?n by a lambda when "?n a" has to	herbelin	2011-03-05
*	Reorganized a bit evarconv.ml:	herbelin	2011-03-05
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Instantiate evar by a lambda when "?n args" has to unify with Prod	herbelin	2011-03-05
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)	letouzey	2011-02-11
*	Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)	letouzey	2011-02-03
*	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey	2011-01-27
*	ratrapage exception, deja fait ...	bgregoir	2011-01-11
*	Fixing an uncaught exception bug with use of vmcast	herbelin	2011-01-07
*	mli comments for doc	pboutill	2011-01-07
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin	2010-12-19
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Refresh universes in params when generating schemes (Closes: #2429)	glondu	2010-11-08
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Slight cosmetic cleaning of tacred.ml.	herbelin	2010-10-31
*	Fixing the Not_found error in bug #2404 + dead code removal in cases.ml	herbelin	2010-10-06
*	Improve handling of metas as evars in unification (patch by Hugo)	letouzey	2010-09-30
*	Speed-up refine by avoiding some calls to Evd.fold	letouzey	2010-09-30
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28