coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Removed a few calls to "Opaque" in Logic.v ineffective since at least	herbelin	2012-10-24
*	No more states/initial.coq, instead coqtop now requires Prelude.vo	letouzey	2012-08-23
*	Updating headers.	herbelin	2012-08-08
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Bug 2767	pboutill	2012-05-09
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	No more use of tauto in Init/	pboutill	2012-01-19
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Take benefit of bullets available by default in Prelude	herbelin	2011-08-10
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...	aspiwack	2011-08-09
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	All the parameters of or can be implicits.	pboutill	2011-07-26
*	Same Implicit Arguments rule for sumbool and sumor.	pboutill	2011-07-26
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	Added a characterization of unique existence.	herbelin	2011-07-16
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Some simplifications in NZDomain	letouzey	2011-06-20
*	Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)	letouzey	2011-05-05
*	Modularization of BinNat + fixes of stdlib	letouzey	2011-05-05
*	Better comments and organisation in Datatypes.v	letouzey	2011-05-05
*	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin	2011-04-28
*	Init: some results in Type should rather be Defined than Qed	letouzey	2011-03-21
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	First release of Vector library.	pboutill	2010-12-10
*	Used multiple lists of implicit arguments to transfer the choices of	herbelin	2010-10-23
*	Using multiple lists of implicit arguments in Program for preserving	herbelin	2010-10-03
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	Bool: shorter and more systematic proofs + an iff lemma about eqb	letouzey	2010-07-16
*	Bool: iff lemmas about or, a reflect inductive, an is_true function	letouzey	2010-07-10
*	clear/revert dependent: restrict to hyp(h) instead of ident(h)	letouzey	2010-06-18
*	New tactic "clear dependent", for the moment in ltac in Init/Tactics	letouzey	2010-06-17
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Arith's min and max placed in Peano (+basic specs max_l and co)	letouzey	2010-02-17
*	CompSpec2Type is used to build functions, it should be Defined, not Qed	letouzey	2010-02-13
*	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey	2010-02-12
*	Init/Logic: commutativity and associativity of /\ and \/	letouzey	2010-01-08
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey	2009-12-09
*	Some lemmas about dependent choice + extensions of Compare_dec +	herbelin	2009-11-16