coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Made that notations to names behave like the names they refer to wrt	herbelin	2009-10-28
\| \| \| \| \| \| \| \| \|	implicit arguments and scope (use Implicit Arguments or Arguments Scope commands instead if not the desired behaviour). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
\| \| \| \| \| \| \| \| \| \| \| \|	Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a notation bug when extending binder_constr with empty levels	herbelin	2009-10-17
\| \| \| \| \| \| \| \| \|	(see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 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
*	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin	2009-04-08
\| \| \| \| \| \| \| \| \| \| \|	Not_found bug in Theorem with) from V8.2 to trunk. - Improving indentation in presence of tabulation and utf-8 when reporting error messages with "^^^^^^". - Updating a few svn:ignore properties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 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
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
\| \| \| \| \| \| \| \| \|	late 2008 Coq WG. - Updated Copyright file wrt JProver. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add new directory for pre-compilation of files needed for further tests.	herbelin	2008-12-02
\| \| \| \| \| \| \|	Application to the test of notation import from within a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un autre bug autour de la gestion des niveaux vides de	herbelin	2008-07-11
\| \| \| \| \| \| \| \| \|	camlp4 (faire l'initialisation dans l'ordre: les sous-niveaux vides, eux-mêmes dans l'ordre, avant de créer le niveau de la notation elle-même). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11220 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Résolution bug #1850 sur notations avec niveaux inconnus de	herbelin	2008-05-26
\| \| \| \| \| \| \|	camlp4. Petit nettoyage en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tests notations	herbelin	2006-04-15
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8720 85f007b7-540e-0410-9357-904b9bb8a0f7