coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	- changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵	notin	2012-02-20
\| \| \| \| \| \| \| \|	available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document the [unify] tactic.	msozeau	2012-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected a careless cut-and-paste in Gallina description which dated back ↵	ppedrot	2012-02-01
\| \| \| \| \| \|	to 2003. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved synchronisation of stdlib index page with current library state.	herbelin	2012-02-01
\| \| \| \| \| \| \| \| \| \|	- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	index-list.html.template: add missing files	pboutill	2012-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqtop and coqc: cleaning description of options in RefMan and manpages.	pboutill	2012-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added documentation for "r foo" in Ltac debugger.	herbelin	2012-01-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin	2012-01-20
\| \| \| \| \| \|	committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the btauto tactic to the documentation.	ppedrot	2012-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin	2011-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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