coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
\|
*	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\
* \|	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
\| \| \| \| \| \| \| \| \| \|	Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
\| *	Fixing another regression with 8.4 wrt to βι-normalization of created hyps.	Hugo Herbelin	2017-08-21
\|/ \| \| \| \| \|	This one is a continuation of e2a8edaf59 which was βι-normalizing the hypotheses created by a "match". We forgot to do it for "let" and "if". This is what this commit is doing.
*	Fix test-suite files after change in refine tactic.	Maxime Dénès	2015-12-15
\| \| \| \|	Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
*	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack	2013-12-06
\|
*	Unset Asymmetric Patterns	pboutill	2013-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin	2008-11-04
\| \| \| \| \| \| \|	Grant wish #1988 ("fun" forces reduction in "refine" if needed) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Wish #1582 (3eme)	herbelin	2007-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug refine	herbelin	2006-11-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9359 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vieux bug de fin 2004 gardé pour mémoire	herbelin	2006-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8792 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bug #1102	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Erreur commit précédent	herbelin	2004-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bug #888	herbelin	2004-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bug #889	herbelin	2004-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout exemple Yves	herbelin	2003-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refine et let-in	filliatr	2001-09-20
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2012 85f007b7-540e-0410-9357-904b9bb8a0f7