coq - The formal proof system

Age	Commit message (Expand)	Author
2013-03-12	A version of Univ.check_eq with no anomaly for Evd.set_eq_sort	letouzey
2013-03-12	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2013-03-12	Allowing different types of, not to be mixed, generic Stores through	ppedrot
2013-03-11	Added a Local Definition vernacular command. This type of definition	ppedrot
2013-03-05	More monomorphization.	ppedrot
2013-02-28	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-26	kernel/declarations becomes a pure mli	letouzey
2013-02-25	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill
2013-02-21	A slightly more efficient test of well-typedness of restriction of	herbelin
2013-02-19	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-18	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-17	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-10	Splitted Evarutil in two files	ppedrot
2013-02-10	Moved code from Pretype_error to Evarutil	ppedrot
2013-02-05	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-01-29	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin
2013-01-28	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-27	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-24	Reductionops: whd_state_gen can take and answers a cst_stack too	pboutill
2013-01-22	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-18	Evarconv: Check stack before term in Canonical Structure approuval	pboutill
2012-12-21	Awful heuristic to refold mutual fixpoint in reductionops	pboutill
2012-12-21	Fixup and comment reductionops	pboutill
2012-12-19	Reductionops reduction machine can refold constant	pboutill
2012-12-19	Evarconv.Pseudorigid erasure	pboutill
2012-12-19	Array.create is deprecated	pboutill
2012-12-18	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-17	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-14	Modulification of dir_path	ppedrot