coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	update Proof General URL	Paul Steckler	2016-08-23
\|
*	RefMan, ch. 4: Rephrasing and moving paragraph on the double reading	Hugo Herbelin	2015-12-10
\| \| \| \|	proof/program of the syntax.
*	RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being	Hugo Herbelin	2015-12-10
\| \| \| \| \| \| \| \| \| \|	clearer that the version depends on the version of Coq. Also renouncing to the "Predicative" and "(Co)" in the name, since after all, usage seems to continue calling the language of Coq Calculus of Inductive Constructions and to consider the Set predicative vs Set impredicative, as well as the presence of coinduction, as flavors of the CIC.
*	Document native_compute.	Maxime Dénès	2015-01-08
\|
*	refman: switch all source files to utf8	Pierre Letouzey	2014-12-09
\| \| \| \| \| \|	Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
*	First stab at documenting Canonical Structures	Enrico Tassi	2013-11-29
\|
*	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau	2013-06-04
\| \| \| \| \| \| \| \| \|	according to a given strategy. - Enhance the hints/lemmas strategy to support "using tac" comming from rewrite hints to solve side-conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 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
*	modifs de nsatz suggerees par Hugo	pottier	2010-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13194 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
\| \| \| \| \| \| \| \| \| \|	- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Micromega: doc + test-suite update	fbesson	2008-07-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add almost empty Classes.tex for documentation of type classes.	msozeau	2008-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10808 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debug implementation of dependent induction/dependent destruction and ↵	msozeau	2008-01-31
\| \| \| \| \| \|	document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Program and its tactics, fix enormous interaction bug due ↵	msozeau	2007-07-19
\| \| \| \| \| \|	to bad cache handling. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation of f_equal and revert and case_eq (and ↵	letouzey	2007-07-05
\| \| \| \| \| \|	s/lri.fr/pps.jussieu.fr/ in my bib entry) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation format biblio	herbelin	2007-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout thèse Cornes	herbelin	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9089 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ biblio	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ de la biblio du manuel de référence	notin	2006-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9062 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update Program/subtac documentation.	msozeau	2006-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8890 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés des fichiers .tex (svn:executable)	notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty	2006-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin	2006-02-23
	principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7