coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
\| \| \| \| \| \|	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey	2008-07-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	In fact, Qge and Ggt disappear, and we only leave notations for > and >= that map directly to Qlt and Qle. We also adopt the same approach for BigN, BigZ, BigQ. By the way, various clean-up concerning Zeq_bool, Zle_bool and similar functions for Q. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clarification de l'ordre d'interprétation des variables dans ltac. En	herbelin	2008-05-01
\| \| \| \| \| \| \| \| \| \| \|	particulier, TacCall(_,f,[]) est utilisé pour une référence à une variable ltac ou une tactique et Reference(f) est utilisé pour une référence à une variable ltac ou un constr (en passant, standardisation de l'utilisation de constr: ou ltac: à setoid_ring). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10878 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
\| \| \| \| \| \| \| \| \|	of the fix I added an optional "by" annotation for rewrite to solve said conditions in the same tactic call. Most of the theories have been updated, only FSets is missing, Pierre will take care of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Solde de code mort et petites optimisations sur lesquels je suis	herbelin	2008-02-09
\| \| \| \| \| \| \|	tombé au cours du temps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
*	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey	2007-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	A file ZOdiv is added which contains results about this euclidean division. Interest compared with Zdiv: ZOdiv implements others (better?) conventions concerning negative numbers, in particular it is compatible with Caml div and mod. ZOdiv is only partially finished... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
*	port de r9968: bug avec les ring calculatoires	barras	2007-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9982 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Orthographe en passant	herbelin	2007-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement dans ring specification du sign, division	bgregoir	2007-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir	2006-12-15
\| \| \| \| \| \| \| \| \|	maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement dans le kernel :	bgregoir	2006-12-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplif de la partie ML de ring/field	barras	2006-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement des _sym par _comm dans setoid_ring	bgregoir	2006-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commit de field + renommages	barras	2006-09-26
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7