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
\|
*	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\|
*	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.
*	Other bugs with "inversion as" (collision between user-provided names and ↵	Hugo Herbelin	2014-09-11
\| \| \| \|	generated equation names).
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
\| \| \| \| \| \| \|	in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
*	Some fixes of the test-suite scripts	letouzey	2011-02-21
\| \| \| \| \| \| \| \|	In particular, the Fail meta-command cannot for the moment catch a Syntax Error, which is raised by Vernac.parse_sentence, before we even now that the line starts by a Fail... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin	2010-06-13
\| \| \| \| \| \|	enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removal of trailing spaces.	serpyc	2009-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin	2009-09-27
\| \| \| \| \| \| \| \| \| \| \| \| \|	which was disturbing inversion and sometimes making it failing in presence of dependent equalities (injection still doesn't know how to split dependent equalities, resulting in a smaller number of equalities than expected for dEqThen). [also restored inv.ml as it was before 12356 which uselessly and inadvertently modified it] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12360 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
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction erreur dans test output Notation.v	herbelin	2008-11-09
\| \| \| \| \| \| \|	- Ajout test pour non-régression du bug #1968 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 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
*	Ajout Unset Implicit Arguments manquant	herbelin	2005-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵	herbelin	2005-03-20
\| \| \| \| \| \|	hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvel exemple; correction du contexte du précédent	herbelin	2004-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrections	herbelin	2004-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout vieil exemple de coq-club	herbelin	2004-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bug #540	herbelin	2004-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin	2003-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test de la correction d'un bug soumis par Dachuan Yu	herbelin	2002-11-06
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3217 85f007b7-540e-0410-9357-904b9bb8a0f7