coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-06-16
*	Fixing printing of Function.	Hugo Herbelin	2016-06-16
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	More toplevel value representation sharing.	Pierre-Marie Pédrot	2016-05-04
*	Revert "Fixing printing of Function."	Hugo Herbelin	2016-04-27
*	Revert "Fixing a mispelling coma -> comma."	Hugo Herbelin	2016-04-27
*	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-04-27
*	Fixing printing of Function.	Hugo Herbelin	2016-04-27
*	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-03-17
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
\|/
*	Partly fixes #3225. Removed some old experimental stuff in funind.	Pierre Courtieu	2015-10-19
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau	2015-10-02
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Function now supports puniveres	jforest	2015-04-14
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Fixing Functional Induction when applied to an alias (reference manual	Hugo Herbelin	2014-11-07
*	Don't raise an error when printing intro-patterns in [functional induction].	Arnaud Spiwack	2014-11-01
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	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-08-18
*	poly: remove unused attribute to STM nodes and vernac classificaiton	Enrico Tassi	2014-05-15
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	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
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Modulification of identifier	ppedrot	2012-12-14