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	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	- Fix comparison of universes.	Matthieu Sozeau
2014-05-06	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-02-24	Reductionops.Stack.strip* are ready to deal with Shift	Pierre Boutillier
2014-02-24	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier
2014-02-12	TC: honor the use_typeclasses flag in pretyping	Enrico Tassi
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-29	Optimization in unification: when checking that the head of a term is an	ppedrot
2013-10-29	Useless array-to-list casts in Unification.	ppedrot
2013-10-29	Do not generate useless argument arrays in whd_* functions.	ppedrot
2013-10-29	- install evar printer for debugging	msozeau
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-10-23	Small optimizations in unification.	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-07-19	- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...	msozeau
2013-06-19	- Keep the refinement of existing evars comming from unification with a rewri...	msozeau
2013-05-10	Little oversight in commit r16489 (fix for bug #3036).	herbelin
2013-05-08	Protection against "Bad recursive type" in w_unify0 (bug #3036).	herbelin
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-25	Fix bug #2989: make unification.ml able to deal with canonical structure in a...	pboutill
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-02-25	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill
2013-02-17	A more informative message when the elimination predicate for	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-05	Revert "Ordered evars by level of dependency in the merging phase of unificat...	herbelin
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-27	Ordered evars by level of dependency in the merging phase of unification	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-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-11-22	Monomorphization (pretyping)	ppedrot
2012-11-08	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot
2012-10-29	Removed many calls to OCaml generic equality. This was done by	ppedrot
2012-10-04	Improving error message when abtraction over goal (abstract_list_all	herbelin
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-09	Unification in Evar_conv uses an abstract machine state	pboutill
2012-08-08	Updating headers.	herbelin
2012-07-20	Reductionops refactoring	pboutill
2012-07-06	Continuing r15459: it helps testing occur-check early in some	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-20	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin