coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	More monomorphization.	ppedrot	2013-03-05
*	compare_stack_shape before ise_stack2 in evar_conv	pboutill	2013-02-28
*	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin	2013-02-28
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	A slightly more efficient test of well-typedness of restriction of	herbelin	2013-02-21
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Classops : avoid some use of Gmap	letouzey	2013-02-19
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Displaying environment and unfolding aliases in "cannot_unify"	herbelin	2013-02-17
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Locating errors from consider_remaining_unif_problems if possible	herbelin	2013-02-17
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Splitted Evarutil in two files	ppedrot	2013-02-10
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Revert "Ordered evars by level of dependency in the merging phase of unificat...	herbelin	2013-02-05
*	Fixed bug #2981 (anomaly NotASort in Retyping due to collision between	herbelin	2013-02-05
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin	2013-01-28
*	Added backtrace information to anomalies	ppedrot	2013-01-28
*	Ordered evars by level of dependency in the merging phase of unification	herbelin	2013-01-27
*	Improving formatting of output of "Test table".	herbelin	2013-01-27
*	Reductionops: whd_state_gen can take and answers a cst_stack too	pboutill	2013-01-24
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	- Fix evarconv so that we have complete eta-conversion:	msozeau	2013-01-22
*	Evarconv: Check stack before term in Canonical Structure approuval	pboutill	2013-01-18
*	Awful heuristic to refold mutual fixpoint in reductionops	pboutill	2012-12-21
*	Fixup and comment reductionops	pboutill	2012-12-21
*	Reductionops reduction machine can refold constant	pboutill	2012-12-19
*	Evarconv.Pseudorigid erasure	pboutill	2012-12-19
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Taking into account the possibility of having a type of type which is	herbelin	2012-12-18
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Factorization of the elim unif flag with the default flag. Since	herbelin	2012-12-18
*	Do not display REVERTcast inserted by reduction tactics (unless printing all).	herbelin	2012-12-17
*	Fixed a bug in the algorithm trying to elaborate a "match" return predicate.	herbelin	2012-12-17
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08