coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-23	Remove undocumented command "Delete foo"	letouzey
2012-03-23	Remove old proof-managment commands Suspend/Resume	letouzey
2012-03-21	Ppvernac: nicer printing of proof delimiters { ... }	letouzey
2012-03-20	Fixing bug #2724 (using notations with binders in cases patterns	herbelin
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-20	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin
2012-03-19	Hopefully complying with camlp5 < 6.00 syntax	herbelin
2012-03-18	Yet another subtlety with bug 2732: when several grammar rules of a	herbelin
2012-03-18	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-03-02	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill
2012-03-02	Noise for nothing	pboutill
2012-02-29	In the syntax of pattern matching, "in" clauses are patterns.	pboutill
2012-02-14	Arguments supports extra notation scopes	gareuselesinge
2012-02-07	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack
2012-01-31	Fix camlp4 compilation	pboutill
2012-01-30	Added an pattern / occurence syntax for vm_compute.	ppedrot
2012-01-23	Removed a seemingly unused argument in Require of modules, introduced 10 year...	ppedrot
2012-01-23	Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.	ppedrot
2012-01-20	Reverted previous commit, which broke library compilation.	ppedrot
2012-01-20	This is a quick hack to permit the parsing of the locality flag in the Progra...	ppedrot
2012-01-20	Fix printing of classes	msozeau
2012-01-19	Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.	msozeau
2012-01-19	Pretty printing of generalized binder	pboutill
2012-01-17	Fixed the pretty-printing of the Program plugin.	ppedrot
2012-01-17	Some fix in beautify pretty-printer	pboutill
2012-01-16	Inductiveops.nb_*{,_env} cleaning	pboutill
2012-01-10	Fix printing of instances, generalized arguments.	msozeau
2011-12-19	Fixed some printing details for dependent evars in emacs mode. Patch	courtieu
2011-12-18	Applied patches proposed suggested by Hendrik Tews to fix existential	courtieu
2011-12-18	Removing PrintConstr debugging entry in g_proof.ml4 which was not	herbelin
2011-12-17	A pass on warning printings. Made systematic the use of msg_warning so	herbelin
2011-12-17	Improving pretty-printing of Ltac functions.	herbelin
2011-12-16	Fixing previous commit which was bugging on tactics preceded by goal number (...	courtieu
2011-12-16	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu
2011-12-12	Proof using ...	gareuselesinge
2011-12-08	Makefile: force the installation of all .cmi (and remove some obsolete .mli)	letouzey
2011-12-07	Fixing grammar resetting bug in the presence of levels initially empty	herbelin
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-12-04	Fixing superflous newline in output of About when no parameter is renamed.	herbelin
2011-11-30	Continuing r14747 being actually incomplete (flushing warnings and	herbelin
2011-11-30	Preventing Implicit Arguments warning to be shown in non verbose mode	herbelin
2011-11-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-11-23	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack
2011-11-21	Renamig support added to "Arguments"	gareuselesinge
2011-11-21	New Arguments vernacular	gareuselesinge
2011-11-18	Adding the type infrastructure to handle properly API management of options	ppedrot
2011-11-18	Fix parsing of :>> and backtrack correctly on the cache of hints for local co...	msozeau
2011-11-18	Added a printing function to handle single evars	ppedrot
2011-11-18	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau