coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Coqide now need lablgtk2.14.0	pboutill	2011-06-11
*	Updated CHANGES (info, Show Script, rephrasing).	herbelin	2011-06-10
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	Fixing the "buggy" first_name and prepare multi-induction.	herbelin	2011-06-10
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
*	Integrating onLastHypId into intro so that we can get the introduction	herbelin	2011-06-10
*	Call process_vernac_interp_error before calling Errors.print in	herbelin	2011-06-10
*	Coqide Menubar integration in MacOS	pboutill	2011-06-10
*	no more errors at _stubs.c.d generation	pboutill	2011-06-10
*	Menubar and toolbar in coqide using GtkUI & Gactions.	pboutill	2011-06-10
*	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill	2011-06-10
*	Fixes in pruning, do not fail if pruning is impossible due to typing constrai...	msozeau	2011-06-10
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	More fixes in pruning/restriction of evars during unification.	msozeau	2011-06-09
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
*	Fixes in pruning in unification.	msozeau	2011-06-08
*	Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...	msozeau	2011-06-07
*	Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...	msozeau	2011-06-07
*	Catch AbstractionOverMeta as a unification failure in precatchable_exception.	msozeau	2011-06-07
*	Fix bug #2415: warn when closing modules or sections and some obligations are...	msozeau	2011-06-07
*	Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.	msozeau	2011-06-07
*	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau	2011-06-07
*	Typo.	gmelquio	2011-06-06
*	Mini-test for eta	herbelin	2011-05-26
*	Partial fix for accepting bound variables with same name as implicit	herbelin	2011-05-26
*	Check if recursive calls are guarded before printing "Proof completed".	herbelin	2011-05-26
*	Fixing discriminate for identity.	herbelin	2011-05-26
*	Q2R -> IQR	fbesson	2011-05-25
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Applying Enrico Tassi's patch for giving priority to delta over eta in	herbelin	2011-05-24
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...	fbesson	2011-05-23
*	ported r14149 from v8.3 branch: bug in checker (redefined global)	barras	2011-05-23
*	Restore display of notation when printing an inductive such as sig	letouzey	2011-05-21
*	added support to handle division by a constant over R	fbesson	2011-05-20
*	Remove useless "open Gc"	glondu	2011-05-19
*	Remove System.process_time (dead code)	glondu	2011-05-19
*	Extraction: avoid lots of late mind_of_kn	letouzey	2011-05-19
*	Extraction: global reference should be indexed on their user part (fix #2540)	letouzey	2011-05-19
*	cbv delta - [...] before calling lia	fbesson	2011-05-18
*	apply zeta reduction before syntaxification	fbesson	2011-05-18
*	Extraction: avoid printing of Recursive Extraction in coqide's console	letouzey	2011-05-18
*	Coqide: allow the use of Abort (grant wish #2357)	letouzey	2011-05-18
*	Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)	letouzey	2011-05-17
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	More work on error handling	letouzey	2011-05-17
*	Add simple test of bullet behaviour.	aspiwack	2011-05-17
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	Fixes bug in [maximal_unfocus] introduced in r14120.	aspiwack	2011-05-17
*	Repair the "Fail" command after recent changes in exception handling	letouzey	2011-05-16