coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Fix #3001 (rename arg of global cst inside section)	gareuselesinge	2013-04-18
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Fix of r16257 in r16205 for "errors raised by check_evar_instance were	herbelin	2013-04-17
*	Like in r16346, do not filter local definitions (here in the	herbelin	2013-04-17
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	Native compiler: timing info for reification in debug mode.	mdenes	2013-03-25
*	Fix bug #2989: make unification.ml able to deal with canonical structure in a...	pboutill	2013-03-25
*	Comments in mli	pboutill	2013-03-25
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Fix bug# 2994, 2971 about better error messages.	msozeau	2013-03-22
*	Fixing unfolding of local definitions during unification that appeared	herbelin	2013-03-21
*	Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.	herbelin	2013-03-21
*	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin	2013-03-21
*	Fixing an old pecularity of "red": head betaiota redexes are now	herbelin	2013-03-21
*	Check a list length before doing a List.chop (fix #3000)	letouzey	2013-03-20
*	Fix for bug #3004 (thanks Hugo!)	letouzey	2013-03-18
*	Avoid a few overzealous "when Errors.noncritical"	letouzey	2013-03-17
*	Retyping.get_type_of: a lax version raising no anomalies	letouzey	2013-03-17
*	Typo in an error message	letouzey	2013-03-14
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey	2013-03-13
*	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-12
*	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