coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Improving pretty-printing of Ltac functions.	herbelin	2011-12-17
*	Fixing format of complexity bug Notations.v.	herbelin	2011-12-17
*	Fixing previous commit which was bugging on tactics preceded by goal number (...	courtieu	2011-12-16
*	Coqide: adapt some comments now that bullets are terminators like { }	letouzey	2011-12-16
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
*	Adapting coqide to my last commit:	courtieu	2011-12-16
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...	ppedrot	2011-12-15
*	Some extra universe refreshing seems needed in abstract_generalize	herbelin	2011-12-14
*	CHANGES: some more updates	letouzey	2011-12-12
*	Proof using ...	gareuselesinge	2011-12-12
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
*	Makefile: force the installation of all .cmi (and remove some obsolete .mli)	letouzey	2011-12-08
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
*	Fixing grammar resetting bug in the presence of levels initially empty	herbelin	2011-12-07
*	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin	2011-12-07
*	Fixing a bug of commit r13310 (activating coercions only when module	herbelin	2011-12-07
*	Html page titles	pboutill	2011-12-07
*	Vectors use a bit more the pattern matching compiler	pboutill	2011-12-07
*	Typo	pboutill	2011-12-07
*	Fixed a synchronization bug between coqtop and the CoqIDE command pane.	ppedrot	2011-12-06
*	fix Makefile.common handling of -byte-only	gareuselesinge	2011-12-06
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
*	Documentation for Arguments + notation scopes	gareuselesinge	2011-12-06
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Backtrack on synchronizing universe counter with reset	herbelin	2011-12-06
*	Registering universe and meta/evar counters as summaries so as to	herbelin	2011-12-05
*	Yet another fix about alias in testing if pattern unification applies.	herbelin	2011-12-05
*	Fixing bugs in doc about when "with" is needed or not to give bindings	herbelin	2011-12-04
*	Fixed a small regression in pattern-matching compilation introduced in	herbelin	2011-12-04
*	A small test for type inference (used to be a regression at some time).	herbelin	2011-12-04
*	Fixing superflous newline in output of About when no parameter is renamed.	herbelin	2011-12-04
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
*	Fixed a bug introduced in r12755. CoqIDE would ignore the Printing Existentia...	ppedrot	2011-11-30
*	Extraction: try to avoid issues with an Include directly inside a .v	letouzey	2011-11-30
*	Now CoqIDE relies on the option query mechanism to set printing options. Stil...	ppedrot	2011-11-30
*	More type safety in query GADT (again).	ppedrot	2011-11-30
*	Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...	ppedrot	2011-11-30
*	Continuing r14747 being actually incomplete (flushing warnings and	herbelin	2011-11-30
*	Quick hack to avoid anomaly on using Program w/o having required JMeq.	herbelin	2011-11-30
*	Preventing Implicit Arguments warning to be shown in non verbose mode	herbelin	2011-11-30
*	Documentation of appcontext	letouzey	2011-11-29
*	Fixed a warning about unused variable introduced in r14731	ppedrot	2011-11-29
*	lib/xml_lexer.ml in .gitignore (produced by a .mll)	letouzey	2011-11-29
*	Extraction: typo in last commit	letouzey	2011-11-29
*	fix for bug #2649	corbinea	2011-11-29
*	Term: properly ignore Casts between Apps in constr_ord	puech	2011-11-29
*	Term: useless conversion to list in constr_ord deleted	puech	2011-11-29