coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Find a more efficient fix for dealing with template universes:	Matthieu Sozeau	2014-05-06
*	Try a new way of handling template universe levels	Matthieu Sozeau	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-05-06
*	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot	2014-04-23
*	Fixing #3262 which revealed a non-progressing, hence looping,	Hugo Herbelin	2014-04-04
*	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-04-01
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	- install evar printer for debugging	msozeau	2013-10-29
*	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-27
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	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-10-22
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Fixing a regression in unification introduced in r16205 (error raised	herbelin	2013-05-14
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	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
*	Fix for bug #3004 (thanks Hugo!)	letouzey	2013-03-18
*	Retyping.get_type_of: a lax version raising no anomalies	letouzey	2013-03-17
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin	2013-02-28
*	A slightly more efficient test of well-typedness of restriction of	herbelin	2013-02-21
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Splitted Evarutil in two files	ppedrot	2013-02-10