coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-02	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey
2014-03-02	Removing generic equality in Syntax plugin.	Pierre-Marie Pédrot
2014-03-02	Adding an equality function over glob_constr	Pierre-Marie Pédrot
2014-03-01	Fixing pervasive comparisons	Pierre-Marie Pédrot
2013-12-22	Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at	Pierre-Marie Pédrot
2013-12-22	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Restore my version of notation_ops.ml now that List.remove_assoc_f is fixed	letouzey
2013-10-24	Oups, repair the compilation (micromega + Morphism_prop)	letouzey
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-08-03	Replacing uses of association lists by maps in notations.	ppedrot
2013-05-05	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin
2013-01-07	Fixup notation printing in patterns	pboutill
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-11-25	Monomorphization (interp)	ppedrot
2012-11-08	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot
2012-09-15	Some documentation and cleaning of CList and Util interfaces.	ppedrot
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-08-08	Updating headers.	herbelin
2012-07-20	Fixup implicits in patterns & notations	pboutill
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-14	Constrextern is allow to use partially applied notations	pboutill
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey