coq - The formal proof system

Age	Commit message (Expand)	Author
2013-05-06	Small cleaning of Evd interface.	ppedrot
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-05-05	Hack to solve a "Bad recursive type" anomaly.	herbelin
2013-05-03	Removing a redundant function from Evd.	ppedrot
2013-04-30	Fix wrong computation of dependency signature in cases raising an uncaught ex...	msozeau
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-22	code simplifications concerning Summary	letouzey
2013-04-18	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-17	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-03	Fix for bug #3017: wrong handling of the unresolvability status	msozeau
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-03-25	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-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-22	Fix bug# 2994, 2971 about better error messages.	msozeau
2013-03-21	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-20	Check a list length before doing a List.chop (fix #3000)	letouzey
2013-03-18	Fix for bug #3004 (thanks Hugo!)	letouzey
2013-03-17	Avoid a few overzealous "when Errors.noncritical"	letouzey
2013-03-17	Retyping.get_type_of: a lax version raising no anomalies	letouzey
2013-03-14	Typo in an error message	letouzey
2013-03-13	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-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