coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot
2014-04-04	Fixing #3262 which revealed a non-progressing, hence looping,	Hugo Herbelin
2014-04-01	Propagating conversion_problem towards (postponed) evar/evar problems.	Hugo Herbelin
2014-04-01	Fixing bug #2900 (evar/evar unif was supposed to be treated in	Hugo Herbelin
2014-03-05	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-10-29	- install evar printer for debugging	msozeau
2013-10-27	Removing useless filter allocation in evar construction.	ppedrot
2013-10-27	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-23	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey
2013-10-22	Removing some generic equalities.	ppedrot
2013-10-22	Removing useless array-to-list and converse casts used in	ppedrot
2013-10-22	Optimizing evar filters. It seems to cost quite a lot in unification,	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-05-14	Fixing a regression in unification introduced in r16205 (error raised	herbelin
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
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-18	Fix for bug #3004 (thanks Hugo!)	letouzey
2013-03-17	Retyping.get_type_of: a lax version raising no anomalies	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-02-28	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin
2013-02-21	A slightly more efficient test of well-typedness of restriction of	herbelin
2013-02-17	Added propagation of evars unification failure reasons for better	herbelin
2013-02-10	Splitted Evarutil in two files	ppedrot