coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-13	Avoid using "subgoals" in the UI, it means the same as "goals"	Jim Fehrle

2016-05-03	Remove extraneous space in coqtop/pg output (bug #4675).	Guillaume Melquiond

2014-10-23	Taking into account factorization of consecutive names of same types	Hugo Herbelin
	in goal context. Note: printing of a declaration was previously done in the context made of the preceding segment of hypotheses, while now it is made in the full context of all hyps (those coming before and after the hyp being printed). As a consequence, constants which could be confused with a variable in the context are now always qualified even if the conflicting variable name is coming later. But why not, that looks somehow more uniform like this.
2007-07-23	removed thesis	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12	Update (test-suite was not successful).	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9988 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19	Test sobriété de la réduction de Intuition	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2350 85f007b7-540e-0410-9357-904b9bb8a0f7