coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| \| \| \| \| \| \| \| \| \|	The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [] https://ncatlab.org/nlab/show/principle+of+equivalence
*	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
*	Fix implicit arguments in sections bug and check for resolution of evars when	msozeau	2008-07-07
\| \| \| \| \| \| \| \| \|	defining records. Fix test-suite script because of new implicit argument setting for DefaultRelation. Fix regression in auto, changing the order of tried lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various fixes:	msozeau	2008-05-15
\| \| \| \| \| \| \| \| \| \| \| \|	- Fix a typo in lowercase_utf8 - Fix generation of signatures in subtac_cases not working for dependent inductive types with dependent indices. - Fix coercion of inductive types generating ill-typed terms. - Fix test script using new syntax for Instances. - Move simpl_existTs to Program.Equality and use it in simpl_depind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 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