coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Monomorphization (parsing)	ppedrot	2012-11-25
*	Fixed #2926:	ppedrot	2012-10-29
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Added support for option Local (at module level) in Tactic Notation.	herbelin	2012-08-11
*	Updating headers.	herbelin	2012-08-08
*	Re-allow Reset in compiled files	letouzey	2012-07-11
*	A prototype implementation of a Print Namespace command.	aspiwack	2012-07-06
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Added a color output to Coqtop.	ppedrot	2012-06-04
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
*	Migrate the grammar entry about "Ltac" into g_vernac.ml4.	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
*	Program: avoid staying in program mode after a failed Program command	letouzey	2012-04-26
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Fix camlp4 compilation	pboutill	2012-01-31
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	Removed a seemingly unused argument in Require of modules, introduced 10 year...	ppedrot	2012-01-23
*	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 typeclass constraint grammar rule to allow `{_ : Reflexive A R}.	msozeau	2012-01-19
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	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-16
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	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-30
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	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
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.	courtieu	2011-07-05
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	G_vernac can be parsed without grammar.cma	letouzey	2011-04-26
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
*	- Remove useless grammar rule	msozeau	2011-03-23