coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Extension of NArith: Nminus, Nmin, etc	letouzey	2007-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* For uniformity, FSetAVL uses Implicit Arguments (a bit)	letouzey	2007-06-07
\| \| \| \| \| \| \| \| \| \| \|	* Some additionnal properties: - two more induction principles on sets - some results about union, filter, etc - Subset is declared to be a Setoid Relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tail0	thery	2007-06-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Gestion espaces dans notation _ = _ :> _	herbelin	2007-06-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mul_norm for Q fixed	thery	2007-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9871 85f007b7-540e-0410-9357-904b9bb8a0f7
*	comparison functions should be Defined not Qed	letouzey	2007-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9867 85f007b7-540e-0410-9357-904b9bb8a0f7
*	As suggested by Pierre Casteran, fold for FSets/FMaps now takes a	letouzey	2007-05-27
\| \| \| \| \| \| \| \|	(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix for bug #1347 (no more Scope pollution by FSets)	letouzey	2007-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Comparaison JMeq/eq_dep	herbelin	2007-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9849 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added Z and Q implementations with int31.	aspiwack	2007-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add_mul_pos uses int31 only	thery	2007-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9845 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pos_mod fixed	thery	2007-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de sqrt312 (racine carree d'un nombre represente comme un	aspiwack	2007-05-15
\| \| \| \| \| \| \| \|	couple de Int31). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
\| \| \| \| \| \| \| \| \|	details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement des opérations sur bool dans l'état initial	herbelin	2007-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création	herbelin	2007-04-25
\| \| \| \| \| \| \|	des schémas d'élimination standard de JMeq, plutôt que "Reset JMeq_rect". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1510	notin	2007-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1499	notin	2007-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparency of Z_lt_le_dec	notin	2007-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplier version of tail_plus	letouzey	2007-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov	2007-04-02
\| \| \| \| \| \| \|	committing the extension of the general sequence operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9743 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation de NArith/BinPos.v suite au commit #9739	notin	2007-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed the definition of extensions of apply to equivalences	emakarov	2007-04-01
\| \| \| \| \| \| \| \| \| \|	(apply -> H, etc.), which prevented Coq compilation. These tactics require an extension of syntax: t1; [t2 \| .. ], which has to be submitted first. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the following theorems to BinPos:	emakarov	2007-03-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Pplus_xO Pmult_Sn_m Pcompare_eq_Lt (a generalization of Pcompare_Gt_Lt) Pcompare_eq_Gt (a generalization of Pcompare_Lt_Gt) Pcompare_refl_id (a generalization of Pcompare_refl) Pcompare_Lt_eq_Lt (a generalization of Pcompare_Lt_Lt) Pcompare_Gt_eq_Gt (a generalization of Pcompare_Gt_Gt) Pcompare_p_Sp Pcompare_p_Sq (one of the defining axioms of < ) Pcompare_1 (1 is the least positive number) Added the following theorems to BinNat: Nrect (defined in terms of new Prect) Nrect_base Nrect_step (the analogout statement in BinPos is called Prect_succ) Nrec_base Nrec_step Nmult_Sn_m Nsucc_0 Ncompare_0 (0 is the least natural number) Ncompare_n_Sm (one of the defining axioms of < ) Also, defined Nind and Nrec in terms of Nrect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9738 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov	2007-03-30
\| \| \| \| \| \| \| \| \|	"apply -> t", "apply <- t", "apply -> t in H" and "apply <- t in H" . Also added the tactic false_hyp based on absurd_hyp. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	stupid me: ?f two times in a pattern	letouzey	2007-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9731 85f007b7-540e-0410-9357-904b9bb8a0f7
*	PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ↵	letouzey	2007-03-26
\| \| \| \| \| \|	OrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9730 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typos	herbelin	2007-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9708 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed an unnecessary argument (p : positive) in Prect_base.	emakarov	2007-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9701 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof simplification for eq_nat_dec et le_lt_dec: induction over	letouzey	2007-03-12
\| \| \| \| \| \| \| \| \|	2nd arg m can simply be a destruct. This helps (vm_)compute __a lot__. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9698 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparence de eq_dec et lt_dec daans OrderedTypeFacts	notin	2007-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 85f007b7-540e-0410-9357-904b9bb8a0f7
*	FSetInterface: new item choose_equal in the spec S (request of P. Casteran)	letouzey	2007-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9684 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajouts de lemmes dans Min et Max	notin	2007-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Autres passages de Set Ã Type dans Relations et Wellfounded	herbelin	2007-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur le passage de Set à Type pour l'ordre lexicographique	herbelin	2007-02-07
\| \| \| \| \| \| \| \|	pour garder Relation_Operators.Pow dans Set (puisque le polymorphisme d'univers pour les inductifs ne se propage pas aux définitions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9598 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction typo eq_rec_eq (cf bug #1339)	herbelin	2007-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov	2007-01-23
\| \| \| \| \| \| \| \|	and countable A. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clarification redondance Axiome du choix unique/description	herbelin	2007-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
\| \| \| \| \| \| \|	égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de la définition de Pind et Prec par une définition	herbelin	2006-12-28
\| \| \| \| \| \| \| \| \|	suggérée par Conor McBride qui ne fait pas intervenir eq_rect et qui permet de montrer "facilement" (mais avec l'axiome K) les équations de réduction de Prec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9465 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
*	Dépendence inutile	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9440 85f007b7-540e-0410-9357-904b9bb8a0f7
*	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug nommage Zgt_trans_succ	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction Open Local Scope (Ring)	bgregoir	2006-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9428 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
*	fixes PR#1269 about function: there is no reason well founded induction is	bertot	2006-11-05
\| \| \| \| \| \|	limited to only Set and not any type in Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7