coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extraction.tex: typo in an Extract Inductive example (fix #2625)	letouzey	2011-10-18
*	mainbiblio.bib : get rid of merge marker from failed merge	letouzey	2011-10-09
*	A new tactic is_var to check whether a term is a goal/section variable	letouzey	2011-10-07
*	Remove 'status' of Program and explain the :> better, as well as referencing ...	msozeau	2011-10-07
*	Updating some links in the FAQ	herbelin	2011-10-01
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev about	herbelin	2011-09-24
*	auto with nocore : disable the use of the core database (wish #2188)	letouzey	2011-09-23
*	doc/refman/Extraction.tex: no need to actually build euclid.ml	letouzey	2011-09-17
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	Several bug reports came from confusions between generalize and set.	pboutill	2011-09-01
*	Bug 2583: Update of the syntax of terms in the reference manual	pboutill	2011-09-01
*	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin	2011-07-16
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
*	coq_makefile documentation in Refman and -h	pboutill	2011-07-07
*	doc/stdlib: Update the list of ZArith files	letouzey	2011-07-04
*	update of Micromega doc	fbesson	2011-06-29
*	refman nsatz	pottier	2011-06-16
*	update of the file list in doc/stdlib	letouzey	2011-05-06
*	Adding "Tactic Notation" in doc index.	herbelin	2011-04-28
*	Documentation typo.	gmelquio	2011-04-15
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
*	remove old traces of SearchIsos (never ported to 7.x nor 8.x)	letouzey	2011-04-12
*	@ in index of refman (last request of bug 2494)	pboutill	2011-04-08
*	Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)	herbelin	2011-04-06
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
*	Update documentation concerning proofs loading (cf last commit)	letouzey	2011-04-03
*	Documentation of the timeout tactical (cf r13917)	letouzey	2011-03-21
*	An option "Set Default Timeout n."	letouzey	2011-03-17
*	Restore documentation of library String which was removed in 2007 (r10049)	herbelin	2011-03-05
*	Remove obsolete TheoryList	glondu	2011-02-10
*	Fix formatting issue in refman	glondu	2011-01-12
*	Remove references to -ide option of coqmktop	glondu	2011-01-11
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Precision in documentation of "decide equality"	glondu	2010-12-24
*	Remove the two-argument variant of "decide equality"	glondu	2010-12-23
*	More precise documentation for instantiate	glondu	2010-12-23
*	Example of a simple ML tactic (Hello world).	fkirchne	2010-12-09
*	Numbers and bitwise functions.	letouzey	2010-12-06
*	Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).	herbelin	2010-12-04
*	Documentation for tactic constr_eq	glondu	2010-12-02
*	Add tactic has_evar (#2433)	glondu	2010-12-02
*	Add tactic is_evar (Closes: #2433)	glondu	2010-12-02
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	Integer division: quot and rem (trunc convention) in addition to div and mod	letouzey	2010-11-10
*	Numbers: axiomatization, properties and implementations of gcd	letouzey	2010-11-05
*	Fix typo in "Hint Extern" doc	glondu	2010-11-03
*	Document DOT output of universe graph	glondu	2010-11-02
*	Numbers : log2. Abstraction, properties and implementations.	letouzey	2010-11-02