coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Version number, copyright, credits: missing updates.	herbelin	2011-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4: More exhaustive list of external contributors.	herbelin	2011-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4 + resetting COMPATIBILITY file.	herbelin	2011-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
\| \| \| \| \| \| \| \| \|	arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof using ...	gareuselesinge	2011-12-12
\| \| \| \| \| \| \| \| \| \| \| \| \|	New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Html page titles	pboutill	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Arguments + notation scopes	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bugs in doc about when "with" is needed or not to give bindings	herbelin	2011-12-04
\| \| \| \| \| \|	to tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of appcontext	letouzey	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc: two minor fixes to make my latex happy	letouzey	2011-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14733 85f007b7-540e-0410-9357-904b9bb8a0f7
*	/home/pirbo/.coqrc* are read again	pboutill	2011-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14714 85f007b7-540e-0410-9357-904b9bb8a0f7
*	-user option removal	pboutill	2011-11-21
\| \| \| \| \| \| \|	it is imcompatible with the freedesktop policy that config directory is private. Feel absolutly free to revert this commit if you think -user should stay git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqrc in the right XDG_CONFIG_HOME/coq folder	pboutill	2011-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIdE configuration file won't pollute your home anymore	pboutill	2011-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add support for XDG_DATA_HOME and XDG_DATA_DIRS.	pboutill	2011-11-20
\| \| \| \| \| \|	From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction.tex: typo in an Extract Inductive example (fix #2625)	letouzey	2011-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mainbiblio.bib : get rid of merge marker from failed merge	letouzey	2011-10-09
\| \| \| \| \| \|	Thanks to Tom Prince for spotting this git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14530 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A new tactic is_var to check whether a term is a goal/section variable	letouzey	2011-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove 'status' of Program and explain the :> better, as well as referencing ↵	msozeau	2011-10-07
\| \| \| \| \| \|	it properly in the syntax of terms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating some links in the FAQ	herbelin	2011-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
\| \| \| \| \| \|	Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev about	herbelin	2011-09-24
\| \| \| \| \| \|	using unicode in X11. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	auto with nocore : disable the use of the core database (wish #2188)	letouzey	2011-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc/refman/Extraction.tex: no need to actually build euclid.ml	letouzey	2011-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05
\| \| \| \| \| \| \| \|	Even if they are no-ops now, the commands Set/Unset Undo themselves are kept for compatibility, in particular to avoid error messages or warnings during the initialization of ProofGeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
\| \| \| \| \| \|	+ s/cbv/lazy of bug 2542 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Several bug reports came from confusions between generalize and set.	pboutill	2011-09-01
\| \| \| \| \| \| \|	Maybe, people will read the two sections of the ref-man at the same time if they are one after the other... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2583: Update of the syntax of terms in the reference manual	pboutill	2011-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin	2011-07-16
\| \| \| \| \| \| \| \| \| \| \|	that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
\| \| \| \| \| \| \| \|	when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile documentation in Refman and -h	pboutill	2011-07-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc/stdlib: Update the list of ZArith files	letouzey	2011-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
*	update of Micromega doc	fbesson	2011-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	refman nsatz	pottier	2011-06-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	update of the file list in doc/stdlib	letouzey	2011-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding "Tactic Notation" in doc index.	herbelin	2011-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation typo.	gmelquio	2011-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
\| \| \| \| \| \| \| \|	This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remove old traces of SearchIsos (never ported to 7.x nor 8.x)	letouzey	2011-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
*	@ in index of refman (last request of bug 2494)	pboutill	2011-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)	herbelin	2011-04-06
\| \| \| \| \| \|	(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
\| \| \| \| \| \| \| \| \|	This is useful, for example, in declaring the projection of the dependent record bundled form of an unbundled typeclass. Patch submitted by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update documentation concerning proofs loading (cf last commit)	letouzey	2011-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of the timeout tactical (cf r13917)	letouzey	2011-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An option "Set Default Timeout n."	letouzey	2011-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restore documentation of library String which was removed in 2007 (r10049)	herbelin	2011-03-05
\| \| \| \| \| \| \|	probably inadvertantly since it is not reported in the commit log. (Thanks to Cédric who noticed it.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove obsolete TheoryList	glondu	2011-02-10
\| \| \| \| \| \| \| \|	This library is no longer used anywhere, and its contents is very... let's say historical... More seriously, many (and presumably the most useful) stuff that used to be there are in List, now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13828 85f007b7-540e-0410-9357-904b9bb8a0f7