coq - The formal proof system

Age	Commit message (Expand)	Author
2016-03-17	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot
2016-03-17	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot
2016-03-17	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot
2016-03-17	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-27	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot
2015-10-19	Partly fixes #3225. Removed some old experimental stuff in funind.	Pierre Courtieu
2015-10-13	Fix some typos.	Guillaume Melquiond
2015-10-02	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau
2015-05-13	Safer typing primitives.	Pierre-Marie Pédrot
2015-04-14	Function now supports puniveres	jforest
2015-01-12	Update headers.	Maxime Dénès
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-11-07	Fixing Functional Induction when applied to an alias (reference manual	Hugo Herbelin
2014-11-01	Don't raise an error when printing intro-patterns in [functional induction].	Arnaud Spiwack
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-08-18	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-18	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-05-15	poly: remove unused attribute to STM nodes and vernac classificaiton	Enrico Tassi
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
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-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-03-02	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey
2014-02-16	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot
2013-12-04	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-08-08	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-10-04	Moved Compat to parsing. This permits to break the dependency of the	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
2012-05-29	slim down a bit genarg.ml (pr_intro_pattern forgotten there)	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-18	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin
2012-03-02	Noise for nothing	pboutill
2011-06-10	Call process_vernac_interp_error before calling Errors.print in	herbelin